Hardened property-based testing framework. More tests, less bugs.

Those end-to-end tests are useful. Both for controlling the behavior of the shrinker, but also to double check the reification of Plutus Data back into untyped expressions.
  I had to work-around a few things to get opaque type and private types play nice. Also found a weird bug due to how we apply parameters after unique debruijn indexes have been also applied. A work-around is to re-intern the program.

crates/aiken-lang/src/ast.rs

@@ -258,6 +258,34 @@ pub struct FunctionAccessKey {
 pub type TypedDataType = DataType<Rc<Type>>;
 
 impl TypedDataType {
+    pub fn bool() -> Self {
+        DataType {
+            constructors: vec![
+                RecordConstructor {
+                    location: Span::empty(),
+                    name: "False".to_string(),
+                    arguments: vec![],
+                    doc: None,
+                    sugar: false,
+                },
+                RecordConstructor {
+                    location: Span::empty(),
+                    name: "True".to_string(),
+                    arguments: vec![],
+                    doc: None,
+                    sugar: false,
+                },
+            ],
+            doc: None,
+            location: Span::empty(),
+            name: "Bool".to_string(),
+            opaque: false,
+            parameters: vec![],
+            public: true,
+            typed_parameters: vec![],
+        }
+    }
+
     pub fn prng() -> Self {
         DataType {
             constructors: vec![

crates/aiken-lang/src/builtins.rs

@@ -1220,6 +1220,16 @@ pub fn prelude_data_types(id_gen: &IdGenerator) -> IndexMap<DataTypeKey, TypedDa
         ordering_data_type,
     );
 
+    // Bool
+    let bool_data_type = TypedDataType::bool();
+    data_types.insert(
+        DataTypeKey {
+            module_name: "".to_string(),
+            defined_type: "Bool".to_string(),
+        },
+        bool_data_type,
+    );
+
     // Option
     let option_data_type = TypedDataType::option(generic_var(id_gen.next()));
     data_types.insert(

crates/aiken-lang/src/expr.rs

@@ -1,22 +1,23 @@
-use std::{collections::HashMap, rc::Rc};
-use uplc::KeyValuePairs;
-
-use vec1::Vec1;
-
-use pallas::ledger::primitives::alonzo::{Constr, PlutusData};
-use uplc::machine::value::from_pallas_bigint;
-
 use crate::{
     ast::{
         self, Annotation, Arg, AssignmentKind, BinOp, ByteArrayFormatPreference, CallArg, Curve,
-        DefinitionLocation, IfBranch, Located, LogicalOpChainKind, ParsedCallArg, Pattern,
+        DataType, DataTypeKey, DefinitionLocation, IfBranch, Located, LogicalOpChainKind,
-        RecordUpdateSpread, Span, TraceKind, TypedClause, TypedRecordUpdateArg, UnOp,
+        ParsedCallArg, Pattern, RecordConstructorArg, RecordUpdateSpread, Span, TraceKind,
-        UntypedClause, UntypedRecordUpdateArg,
+        TypedClause, TypedDataType, TypedRecordUpdateArg, UnOp, UntypedClause,
+        UntypedRecordUpdateArg,
     },
     builtins::void,
+    gen_uplc::builder::{
+        check_replaceable_opaque_type, convert_opaque_type, lookup_data_type_by_tipo,
+    },
     parser::token::Base,
-    tipo::{ModuleValueConstructor, PatternConstructor, Type, TypeInfo, TypeVar, ValueConstructor},
+    tipo::{ModuleValueConstructor, PatternConstructor, Type, TypeVar, ValueConstructor},
 };
+use indexmap::IndexMap;
+use pallas::ledger::primitives::alonzo::{Constr, PlutusData};
+use std::rc::Rc;
+use uplc::{machine::value::from_pallas_bigint, KeyValuePairs};
+use vec1::Vec1;
 
 #[derive(Debug, Clone, PartialEq)]
 pub enum TypedExpr {
@@ -584,7 +585,7 @@ impl UntypedExpr {
     // The function performs some sanity check to ensure that the type does indeed somewhat
     // correspond to the data being given.
     pub fn reify(
-        data_types: &HashMap<String, TypeInfo>,
+        data_types: &IndexMap<DataTypeKey, &TypedDataType>,
         data: PlutusData,
         tipo: &Type,
     ) -> Result<Self, String> {
@@ -594,6 +595,36 @@ impl UntypedExpr {
             }
         }
 
+        // NOTE: Opaque types are tricky. We can't tell from a type only if it is
+        // opaque or not. We have to lookup its datatype definition.
+        //
+        // Also, we can't -- in theory -- peak into an opaque type. More so, if it
+        // has a single constructor with a single argument, it is an zero-cost
+        // wrapper. That means the underlying PlutusData has no residue of that
+        // wrapper. So we have to manually reconstruct it before crawling further
+        // down the type tree.
+        if check_replaceable_opaque_type(tipo, data_types) {
+            let DataType { name, .. } = lookup_data_type_by_tipo(data_types, tipo)
+                .expect("Type just disappeared from known types? {tipo:?}");
+
+            let inner_type = convert_opaque_type(&tipo.clone().into(), data_types, false);
+
+            let value = UntypedExpr::reify(data_types, data, &inner_type)?;
+
+            return Ok(UntypedExpr::Call {
+                location: Span::empty(),
+                arguments: vec![CallArg {
+                    label: None,
+                    location: Span::empty(),
+                    value,
+                }],
+                fun: Box::new(UntypedExpr::Var {
+                    name,
+                    location: Span::empty(),
+                }),
+            });
+        }
+
         match data {
             PlutusData::BigInt(ref i) => Ok(UntypedExpr::UInt {
                 location: Span::empty(),
@@ -655,68 +686,52 @@ impl UntypedExpr {
                     tag as usize - 1280 + 7
                 };
 
-                if let Type::App { module, name, .. } = tipo {
+                if let Type::App { .. } = tipo {
-                    let module = if module.is_empty() { "aiken" } else { module };
+                    if let Some(DataType { constructors, .. }) =
-                    if let Some(type_info) = data_types.get(module) {
+                        lookup_data_type_by_tipo(data_types, tipo)
-                        if let Some(constructors) = type_info.types_constructors.get(name) {
+                    {
                         let constructor = &constructors[ix];
+
                         return if fields.is_empty() {
                             Ok(UntypedExpr::Var {
                                 location: Span::empty(),
-                                    name: constructor.to_string(),
+                                name: constructor.name.to_string(),
                             })
                         } else {
-                                // NOTE: When the type is _private_, we cannot see the
+                            let arguments = fields
-                                // value constructor and so we default to showing a
-                                // placeholder.
-                                let arguments = match type_info.values.get(constructor) {
-                                    None => Ok(fields
-                                        .iter()
-                                        .map(|_| CallArg {
-                                            label: None,
-                                            location: Span::empty(),
-                                            value: UntypedExpr::Var {
-                                                name: "<hidden>".to_string(),
-                                                location: Span::empty(),
-                                            },
-                                        })
-                                        .collect()),
-                                    Some(value) => {
-                                        let types =
-                                            if let Type::Fn { args, .. } = value.tipo.as_ref() {
-                                                &args[..]
-                                            } else {
-                                                &[]
-                                            };
-
-                                        fields
                                 .into_iter()
-                                            .zip(types)
+                                .zip(constructor.arguments.iter())
-                                            .map(|(field, tipo)| {
+                                .map(
-                                                UntypedExpr::reify(data_types, field, tipo).map(
+                                    |(
-                                                    |value| CallArg {
+                                        field,
-                                                        label: None,
+                                        RecordConstructorArg {
+                                            ref label,
+                                            ref tipo,
+                                            ..
+                                        },
+                                    )| {
+                                        UntypedExpr::reify(data_types, field, tipo).map(|value| {
+                                            CallArg {
+                                                label: label.clone(),
                                                 location: Span::empty(),
                                                 value,
+                                            }
+                                        })
                                     },
                                 )
-                                            })
+                                .collect::<Result<Vec<_>, _>>()?;
-                                            .collect::<Result<Vec<_>, _>>()
-                                    }
-                                }?;
 
                             Ok(UntypedExpr::Call {
                                 location: Span::empty(),
                                 arguments,
                                 fun: Box::new(UntypedExpr::Var {
-                                        name: constructor.to_string(),
+                                    name: constructor.name.to_string(),
                                     location: Span::empty(),
                                 }),
                             })
                         };
                     }
                 }
-                }
 
                 Err(format!(
                     "invalid type annotation {tipo:?} for constructor: {tag:?} with {fields:?}"

crates/aiken-lang/src/gen_uplc.rs

@@ -53,7 +53,7 @@ use uplc::{
 #[derive(Clone)]
 pub struct CodeGenerator<'a> {
     /// immutable index maps
-    pub functions: IndexMap<FunctionAccessKey, &'a TypedFunction>,
+    functions: IndexMap<FunctionAccessKey, &'a TypedFunction>,
     data_types: IndexMap<DataTypeKey, &'a TypedDataType>,
     module_types: IndexMap<&'a String, &'a TypeInfo>,
     module_src: IndexMap<String, (String, LineNumbers)>,
@@ -255,7 +255,7 @@ impl<'a> CodeGenerator<'a> {
                 panic!("Dangling expressions without an assignment")
             };
 
-            let replaced_type = convert_opaque_type(tipo, &self.data_types);
+            let replaced_type = convert_opaque_type(tipo, &self.data_types, true);
 
             let air_value = self.build(value, module_build_name, &[]);
 
@@ -895,7 +895,7 @@ impl<'a> CodeGenerator<'a> {
                 if props.full_check {
                     let mut index_map = IndexMap::new();
 
-                    let non_opaque_tipo = convert_opaque_type(tipo, &self.data_types);
+                    let non_opaque_tipo = convert_opaque_type(tipo, &self.data_types, true);
 
                     let val = AirTree::local_var(name, tipo.clone());
 
@@ -933,7 +933,7 @@ impl<'a> CodeGenerator<'a> {
                     let name = &format!("__discard_expect_{}", name);
                     let mut index_map = IndexMap::new();
 
-                    let non_opaque_tipo = convert_opaque_type(tipo, &self.data_types);
+                    let non_opaque_tipo = convert_opaque_type(tipo, &self.data_types, true);
 
                     let val = AirTree::local_var(name, tipo.clone());
 
@@ -1326,7 +1326,7 @@ impl<'a> CodeGenerator<'a> {
         msg_func: Option<AirMsg>,
     ) -> AirTree {
         assert!(tipo.get_generic().is_none());
-        let tipo = &convert_opaque_type(tipo, &self.data_types);
+        let tipo = &convert_opaque_type(tipo, &self.data_types, true);
 
         if tipo.is_primitive() {
             // Since we would return void anyway and ignore then we can just return value here and ignore
@@ -2775,7 +2775,7 @@ impl<'a> CodeGenerator<'a> {
 
                     let param = AirTree::local_var(&arg_name, data());
 
-                    let actual_type = convert_opaque_type(&arg.tipo, &self.data_types);
+                    let actual_type = convert_opaque_type(&arg.tipo, &self.data_types, true);
 
                     let msg_func = match self.tracing {
                         TraceLevel::Silent => None,
@@ -3632,12 +3632,13 @@ impl<'a> CodeGenerator<'a> {
                     let mut function_def_types = function_def
                         .arguments
                         .iter()
-                        .map(|arg| convert_opaque_type(&arg.tipo, &self.data_types))
+                        .map(|arg| convert_opaque_type(&arg.tipo, &self.data_types, true))
                         .collect_vec();
 
                     function_def_types.push(convert_opaque_type(
                         &function_def.return_type,
                         &self.data_types,
+                        true,
                     ));
 
                     let mono_types: IndexMap<u64, Rc<Type>> = if !function_def_types.is_empty() {

crates/aiken-lang/src/gen_uplc/builder.rs

@@ -347,6 +347,7 @@ pub fn get_arg_type_name(tipo: &Type) -> String {
 pub fn convert_opaque_type(
     t: &Rc<Type>,
     data_types: &IndexMap<DataTypeKey, &TypedDataType>,
+    deep: bool,
 ) -> Rc<Type> {
     if check_replaceable_opaque_type(t, data_types) && matches!(t.as_ref(), Type::App { .. }) {
         let data_type = lookup_data_type_by_tipo(data_types, t).unwrap();
@@ -363,7 +364,11 @@ pub fn convert_opaque_type(
 
         let mono_type = find_and_replace_generics(generic_type, &mono_types);
 
-        convert_opaque_type(&mono_type, data_types)
+        if deep {
+            convert_opaque_type(&mono_type, data_types, deep)
+        } else {
+            mono_type
+        }
     } else {
         match t.as_ref() {
             Type::App {
@@ -374,7 +379,7 @@ pub fn convert_opaque_type(
             } => {
                 let mut new_args = vec![];
                 for arg in args {
-                    let arg = convert_opaque_type(arg, data_types);
+                    let arg = convert_opaque_type(arg, data_types, deep);
                     new_args.push(arg);
                 }
                 Type::App {
@@ -388,11 +393,11 @@ pub fn convert_opaque_type(
             Type::Fn { args, ret } => {
                 let mut new_args = vec![];
                 for arg in args {
-                    let arg = convert_opaque_type(arg, data_types);
+                    let arg = convert_opaque_type(arg, data_types, deep);
                     new_args.push(arg);
                 }
 
-                let ret = convert_opaque_type(ret, data_types);
+                let ret = convert_opaque_type(ret, data_types, deep);
 
                 Type::Fn {
                     args: new_args,
@@ -402,7 +407,7 @@ pub fn convert_opaque_type(
             }
             Type::Var { tipo: var_tipo } => {
                 if let TypeVar::Link { tipo } = &var_tipo.borrow().clone() {
-                    convert_opaque_type(tipo, data_types)
+                    convert_opaque_type(tipo, data_types, deep)
                 } else {
                     t.clone()
                 }
@@ -410,7 +415,7 @@ pub fn convert_opaque_type(
             Type::Tuple { elems } => {
                 let mut new_elems = vec![];
                 for arg in elems {
-                    let arg = convert_opaque_type(arg, data_types);
+                    let arg = convert_opaque_type(arg, data_types, deep);
                     new_elems.push(arg);
                 }
                 Type::Tuple { elems: new_elems }.into()
@@ -420,7 +425,7 @@ pub fn convert_opaque_type(
 }
 
 pub fn check_replaceable_opaque_type(
-    t: &Rc<Type>,
+    t: &Type,
     data_types: &IndexMap<DataTypeKey, &TypedDataType>,
 ) -> bool {
     let data_type = lookup_data_type_by_tipo(data_types, t);
@@ -633,7 +638,7 @@ pub fn erase_opaque_type_operations(
     let mut held_types = air_tree.mut_held_types();
 
     while let Some(tipo) = held_types.pop() {
-        *tipo = convert_opaque_type(tipo, data_types);
+        *tipo = convert_opaque_type(tipo, data_types, true);
     }
 }
 

crates/aiken-lang/src/tipo/error.rs

@@ -1,7 +1,7 @@
 use super::Type;
-use crate::error::ExtraData;
 use crate::{
     ast::{Annotation, BinOp, CallArg, LogicalOpChainKind, Span, UntypedPattern},
+    error::ExtraData,
     expr::{self, UntypedExpr},
     format::Formatter,
     levenshtein,
@@ -261,7 +261,9 @@ You can use '{discard}' and numbers to distinguish between similar names.
 
     #[error("I found a type definition that has a function type in it. This is not allowed.\n")]
     #[diagnostic(code("illegal::function_in_type"))]
-    #[diagnostic(help("Data-types can't hold functions. If you want to define method-like functions, group the type definition and the methods under a common namespace in a standalone module."))]
+    #[diagnostic(help(
+        "Data-types can't hold functions. If you want to define method-like functions, group the type definition and the methods under a common namespace in a standalone module."
+    ))]
     FunctionTypeInData {
         #[label]
         location: Span,
@@ -477,9 +479,13 @@ If you really meant to return that last expression, try to replace it with the f
         "I stumbled upon an invalid (non-local) clause guard '{}'.\n",
         name.if_supports_color(Stdout, |s| s.purple())
     )]
-    #[diagnostic(url("https://aiken-lang.org/language-tour/control-flow#checking-equality-and-ordering-in-patterns"))]
+    #[diagnostic(url(
+        "https://aiken-lang.org/language-tour/control-flow#checking-equality-and-ordering-in-patterns"
+    ))]
     #[diagnostic(code("illegal::clause_guard"))]
-    #[diagnostic(help("There are some conditions regarding what can be used in a guard. Values must be either local to the function, or defined as module constants. You can't use functions or records in there."))]
+    #[diagnostic(help(
+        "There are some conditions regarding what can be used in a guard. Values must be either local to the function, or defined as module constants. You can't use functions or records in there."
+    ))]
     NonLocalClauseGuardVariable {
         #[label]
         location: Span,
@@ -492,7 +498,7 @@ If you really meant to return that last expression, try to replace it with the f
     #[diagnostic(url("https://aiken-lang.org/language-tour/primitive-types#tuples"))]
     #[diagnostic(code("illegal::tuple_index"))]
     #[diagnostic(help(
-        r#"Because you used a tuple-index on an element, I assumed it had to be a tuple or some kind, but instead I found:
+        r#"Because you used a tuple-index on an element, I assumed it had to be a tuple but instead I found something of type:
 
 ╰─▶ {type_info}"#,
         type_info = tipo.to_pretty(0).if_supports_color(Stdout, |s| s.red())
@@ -637,7 +643,9 @@ You can help me by providing a type-annotation for 'x', as such:
     #[error("I almost got caught in an endless loop while inferring a recursive type.\n")]
     #[diagnostic(url("https://aiken-lang.org/language-tour/custom-types#type-annotations"))]
     #[diagnostic(code("missing::type_annotation"))]
-    #[diagnostic(help("I have several aptitudes, but inferring recursive types isn't one them. It is still possible to define recursive types just fine, but I will need a little help in the form of type annotation to infer their types should they show up."))]
+    #[diagnostic(help(
+        "I have several aptitudes, but inferring recursive types isn't one them. It is still possible to define recursive types just fine, but I will need a little help in the form of type annotation to infer their types should they show up."
+    ))]
     RecursiveType {
         #[label]
         location: Span,
@@ -961,7 +969,8 @@ The best thing to do from here is to remove it."#))]
     #[error("I choked on a generic type left in an outward-facing interface.\n")]
     #[diagnostic(code("illegal::generic_in_abi"))]
     #[diagnostic(help(
-        "Functions of the outer-most parts of a project, such as a validator or a property-based test, must be fully instantiated. That means they can no longer carry unbound generic variables. The type must be fully-known at this point since many structural validation must occur to ensure a safe boundary between the on-chain and off-chain worlds."))]
+        "Functions of the outer-most parts of a project, such as a validator or a property-based test, must be fully instantiated. That means they can no longer carry unbound generic variables. The type must be fully-known at this point since many structural validation must occur to ensure a safe boundary between the on-chain and off-chain worlds."
+    ))]
     GenericLeftAtBoundary {
         #[label("unbound generic at boundary")]
         location: Span,

crates/aiken-lang/src/tipo/infer.rs

@@ -1,5 +1,10 @@
-use std::{borrow::Borrow, collections::HashMap, ops::Deref, rc::Rc};
+use super::{
-
+    environment::{generalise, EntityKind, Environment},
+    error::{Error, UnifyErrorSituation, Warning},
+    expr::ExprTyper,
+    hydrator::Hydrator,
+    TypeInfo, ValueConstructor, ValueConstructorVariant,
+};
 use crate::{
     ast::{
         Annotation, Arg, ArgName, ArgVia, DataType, Definition, Function, Layer, ModuleConstant,
@@ -14,14 +19,7 @@ use crate::{
     tipo::{Span, Type, TypeVar},
     IdGenerator,
 };
-
+use std::{borrow::Borrow, collections::HashMap, ops::Deref, rc::Rc};
-use super::{
-    environment::{generalise, EntityKind, Environment},
-    error::{Error, UnifyErrorSituation, Warning},
-    expr::ExprTyper,
-    hydrator::Hydrator,
-    TypeInfo, ValueConstructor, ValueConstructorVariant,
-};
 
 impl UntypedModule {
     pub fn infer(
@@ -347,6 +345,21 @@ fn infer_definition(
                     let (inferred_annotation, inner_type) =
                         infer_fuzzer(environment, &typed_via.tipo(), &arg.via.location())?;
 
+                    // Replace the pre-registered type for the test function, to allow inferring
+                    // the function body with the right type arguments.
+                    let scope = environment
+                        .scope
+                        .get_mut(&f.name)
+                        .expect("Could not find preregistered type for test");
+                    if let Type::Fn { ref ret, .. } = scope.tipo.as_ref() {
+                        scope.tipo = Rc::new(Type::Fn {
+                            ret: ret.clone(),
+                            args: vec![inner_type.clone()],
+                        })
+                    }
+
+                    // Ensure that the annotation, if any, matches the type inferred from the
+                    // Fuzzer.
                     if let Some(ref provided_annotation) = arg.annotation {
                         let hydrator: &mut Hydrator = hydrators.get_mut(&f.name).unwrap();
 

crates/aiken-project/src/lib.rs

@@ -30,7 +30,7 @@ use crate::{
 };
 use aiken_lang::{
     ast::{
-        DataTypeKey, Definition, FunctionAccessKey, ModuleKind, Tracing, TypedDataType,
+        DataTypeKey, Definition, FunctionAccessKey, ModuleKind, TraceLevel, Tracing, TypedDataType,
         TypedFunction, Validator,
     },
     builtins,
@@ -810,6 +810,13 @@ where
     fn run_tests(&self, tests: Vec<Test>) -> Vec<TestResult<UntypedExpr>> {
         use rayon::prelude::*;
 
+        let generator = self.checked_modules.new_generator(
+            &self.functions,
+            &self.data_types,
+            &self.module_types,
+            Tracing::All(TraceLevel::Silent),
+        );
+
         tests
             .into_par_iter()
             .map(|test| match test {
@@ -820,7 +827,7 @@ where
             })
             .collect::<Vec<TestResult<PlutusData>>>()
             .into_iter()
-            .map(|test| test.reify(&self.module_types))
+            .map(|test| test.reify(generator.data_types()))
             .collect()
     }
 

crates/aiken-project/src/test_framework.rs

@@ -1,32 +1,31 @@
 use crate::pretty;
 use aiken_lang::{
-    ast::{BinOp, Span, TypedTest},
+    ast::{BinOp, DataTypeKey, Span, TypedDataType, TypedTest},
     expr::{TypedExpr, UntypedExpr},
     gen_uplc::{
         builder::{convert_data_to_type, convert_opaque_type},
         CodeGenerator,
     },
-    tipo::{Type, TypeInfo},
+    tipo::Type,
 };
+use indexmap::IndexMap;
 use pallas::{
     codec::utils::Int,
     ledger::primitives::alonzo::{BigInt, Constr, PlutusData},
 };
 use std::{
     borrow::Borrow,
-    collections::HashMap,
     fmt::{self, Display},
     path::PathBuf,
     rc::Rc,
 };
 use uplc::{
-    ast::{Constant, Data, NamedDeBruijn, Program, Term},
+    ast::{Constant, Data, Name, NamedDeBruijn, Program, Term},
     machine::{cost_model::ExBudget, eval_result::EvalResult},
+    parser::interner::Interner,
 };
 
-/// ----------------------------------------------------------------------------
+/// ----- Test -----------------------------------------------------------------
-///
-/// Test
 ///
 /// Aiken supports two kinds of tests: unit and property. A unit test is a simply
 /// UPLC program which returns must be a lambda that returns a boolean.
@@ -42,7 +41,7 @@ use uplc::{
 /// Our approach could perhaps be called "microthesis", as it implements a subset of
 /// minithesis. More specifically, we do not currently support pre-conditions, nor
 /// targets.
-/// ----------------------------------------------------------------------------
+///
 #[derive(Debug, Clone)]
 pub enum Test {
     UnitTest(UnitTest),
@@ -75,8 +74,8 @@ impl Test {
         module: String,
         name: String,
         can_error: bool,
-        program: Program<NamedDeBruijn>,
+        program: Program<Name>,
-        fuzzer: Fuzzer<NamedDeBruijn>,
+        fuzzer: Fuzzer<Name>,
     ) -> Test {
         Test::PropertyTest(PropertyTest {
             input_path,
@@ -131,7 +130,7 @@ impl Test {
 
             let via = parameter.via.clone();
 
-            let type_info = convert_opaque_type(&parameter.tipo, generator.data_types());
+            let type_info = parameter.tipo.clone();
 
             // TODO: Possibly refactor 'generate_raw' to accept arguments and do this wrapping
             // itself.
@@ -147,17 +146,9 @@ impl Test {
                 return_annotation: None,
             };
 
-            let program = generator
+            let program = generator.clone().generate_raw(&body, &module_name);
-                .clone()
-                .generate_raw(&body, &module_name)
-                .try_into()
-                .unwrap();
 
-            let fuzzer: Program<NamedDeBruijn> = generator
+            let fuzzer = generator.clone().generate_raw(&via, &module_name);
-                .clone()
-                .generate_raw(&via, &module_name)
-                .try_into()
-                .unwrap();
 
             Self::property_test(
                 input_path,
@@ -167,6 +158,11 @@ impl Test {
                 program,
                 Fuzzer {
                     program: fuzzer,
+                    stripped_type_info: convert_opaque_type(
+                        &type_info,
+                        generator.data_types(),
+                        true,
+                    ),
                     type_info,
                 },
             )
@@ -174,12 +170,8 @@ impl Test {
     }
 }
 
-// ----------------------------------------------------------------------------
+/// ----- UnitTest -----------------------------------------------------------------
-//
+///
-// UnitTest
-//
-// ----------------------------------------------------------------------------
-
 #[derive(Debug, Clone)]
 pub struct UnitTest {
     pub input_path: PathBuf,
@@ -205,20 +197,16 @@ impl UnitTest {
     }
 }
 
-// ----------------------------------------------------------------------------
+/// ----- PropertyTest -----------------------------------------------------------------
-//
+///
-// PropertyTest
-//
-// ----------------------------------------------------------------------------
-
 #[derive(Debug, Clone)]
 pub struct PropertyTest {
     pub input_path: PathBuf,
     pub module: String,
     pub name: String,
     pub can_error: bool,
-    pub program: Program<NamedDeBruijn>,
+    pub program: Program<Name>,
-    pub fuzzer: Fuzzer<NamedDeBruijn>,
+    pub fuzzer: Fuzzer<Name>,
 }
 
 unsafe impl Send for PropertyTest {}
@@ -226,7 +214,13 @@ unsafe impl Send for PropertyTest {}
 #[derive(Debug, Clone)]
 pub struct Fuzzer<T> {
     pub program: Program<T>,
+
     pub type_info: Rc<Type>,
+
+    /// A version of the Fuzzer's type that has gotten rid of
+    /// all erasable opaque type. This is needed in order to
+    /// generate Plutus data with the appropriate shape.
+    pub stripped_type_info: Rc<Type>,
 }
 
 impl PropertyTest {
@@ -239,7 +233,7 @@ impl PropertyTest {
 
         let (counterexample, iterations) = match self.run_n_times(n, seed, None) {
             None => (None, n),
-            Some((remaining, counterexample)) => (Some(counterexample), n - remaining + 1),
+            Some((remaining, counterexample)) => (Some(counterexample.value), n - remaining + 1),
         };
 
         TestResult::PropertyTestResult(PropertyTestResult {
@@ -249,12 +243,12 @@ impl PropertyTest {
         })
     }
 
-    fn run_n_times(
+    fn run_n_times<'a>(
-        &self,
+        &'a self,
         remaining: usize,
         seed: u32,
-        counterexample: Option<(usize, PlutusData)>,
+        counterexample: Option<(usize, Counterexample<'a>)>,
-    ) -> Option<(usize, PlutusData)> {
+    ) -> Option<(usize, Counterexample<'a>)> {
         // We short-circuit failures in case we have any. The counterexample is already simplified
         // at this point.
         if remaining > 0 && counterexample.is_none() {
@@ -269,7 +263,7 @@ impl PropertyTest {
         }
     }
 
-    fn run_once(&self, seed: u32) -> (u32, Option<PlutusData>) {
+    fn run_once(&self, seed: u32) -> (u32, Option<Counterexample<'_>>) {
         let (next_prng, value) = Prng::from_seed(seed)
             .sample(&self.fuzzer.program)
             .expect("running seeded Prng cannot fail.");
@@ -291,7 +285,7 @@ impl PropertyTest {
                     counterexample.simplify();
                 }
 
-                (next_seed, Some(counterexample.value))
+                (next_seed, Some(counterexample))
             } else {
                 (next_seed, None)
             }
@@ -301,19 +295,37 @@ impl PropertyTest {
     }
 
     pub fn eval(&self, value: &PlutusData) -> EvalResult {
-        let term = convert_data_to_type(Term::data(value.clone()), &self.fuzzer.type_info)
+        let term: Term<Name> =
-            .try_into()
+            convert_data_to_type(Term::data(value.clone()), &self.fuzzer.stripped_type_info);
-            .expect("safe conversion from Name -> NamedDeBruijn");
+
-        self.program.apply_term(&term).eval(ExBudget::max())
+        let mut program = self.program.apply_term(&term);
+
+        Interner::new().program(&mut program);
+
+        Program::<NamedDeBruijn>::try_from(program)
+            .unwrap()
+            .eval(ExBudget::max())
     }
 }
 
-// ----------------------------------------------------------------------------
+/// ----- PRNG -----------------------------------------------------------------
-//
+///
-// Prng
+/// A Pseudo-random generator (PRNG) used to produce random values for fuzzers.
-//
+/// Note that the randomness isn't actually managed by the Rust framework, it
-// ----------------------------------------------------------------------------
+/// entirely relies on properties of hashing algorithm on-chain (e.g. blake2b).
-
+///
+/// The PRNG can have two forms:
+///
+/// 1. Seeded: which occurs during the initial run of a property. Each time a
+///    number is drawn from the PRNG, a new seed is created. We retain all the
+///    choices drawn in a _choices_ vector.
+///
+/// 2. Replayed: which is used to replay a Prng sequenced from a list of known
+///    choices. This happens when shrinking an example. Instead of trying to
+///    shrink the value directly, we shrink the PRNG sequence with the hope that
+///    it will generate a smaller value. This implies that generators tend to
+///    generate smaller values when drawing smaller numbers.
+///
 #[derive(Debug)]
 pub enum Prng {
     Seeded {
@@ -385,9 +397,9 @@ impl Prng {
     }
 
     /// Generate a pseudo-random value from a fuzzer using the given PRNG.
-    pub fn sample(&self, fuzzer: &Program<NamedDeBruijn>) -> Option<(Prng, PlutusData)> {
+    pub fn sample(&self, fuzzer: &Program<Name>) -> Option<(Prng, PlutusData)> {
-        let result = fuzzer
+        let result = Program::<NamedDeBruijn>::try_from(fuzzer.apply_data(self.uplc()))
-            .apply_data(self.uplc())
+            .unwrap()
             .eval(ExBudget::max())
             .result()
             .expect("Fuzzer crashed?");
@@ -464,14 +476,12 @@ impl Prng {
     }
 }
 
-// ----------------------------------------------------------------------------
+/// ----- Counterexample -----------------------------------------------------------------
-//
+///
-// Counterexample
+/// A counterexample is constructed from a test failure. It holds a value, and a sequence
-//
+/// of random choices that led to this value. It holds a reference to the underlying
-// A counterexample is constructed on test failures.
+/// property and fuzzer. In many cases, a counterexample can be simplified (a.k.a "shrinked")
-//
+/// into a smaller counterexample.
-// ----------------------------------------------------------------------------
-
 #[derive(Debug)]
 pub struct Counterexample<'a> {
     pub value: PlutusData,
@@ -690,7 +700,10 @@ pub enum TestResult<T> {
 unsafe impl<T> Send for TestResult<T> {}
 
 impl TestResult<PlutusData> {
-    pub fn reify(self, data_types: &HashMap<String, TypeInfo>) -> TestResult<UntypedExpr> {
+    pub fn reify(
+        self,
+        data_types: &IndexMap<DataTypeKey, &TypedDataType>,
+    ) -> TestResult<UntypedExpr> {
         match self {
             TestResult::UnitTestResult(test) => TestResult::UnitTestResult(test),
             TestResult::PropertyTestResult(test) => {
@@ -789,7 +802,10 @@ pub struct PropertyTestResult<T> {
 unsafe impl<T> Send for PropertyTestResult<T> {}
 
 impl PropertyTestResult<PlutusData> {
-    pub fn reify(self, data_types: &HashMap<String, TypeInfo>) -> PropertyTestResult<UntypedExpr> {
+    pub fn reify(
+        self,
+        data_types: &IndexMap<DataTypeKey, &TypedDataType>,
+    ) -> PropertyTestResult<UntypedExpr> {
         PropertyTestResult {
             counterexample: match self.counterexample {
                 None => None,
@@ -882,16 +898,19 @@ mod test {
     use crate::module::{CheckedModule, CheckedModules};
     use aiken_lang::{
         ast::{Definition, ModuleKind, TraceLevel, Tracing},
-        builtins, parser,
+        builtins,
+        format::Formatter,
+        parser,
         parser::extra::ModuleExtra,
         IdGenerator,
     };
     use indoc::indoc;
+    use std::collections::HashMap;
 
     const TEST_KIND: ModuleKind = ModuleKind::Lib;
 
     impl Test {
-        pub fn from_source(src: &str) -> Self {
+        pub fn from_source(src: &str) -> (Self, IndexMap<DataTypeKey, TypedDataType>) {
             let id_gen = IdGenerator::new();
 
             let module_name = "";
@@ -924,6 +943,22 @@ mod test {
                 .last()
                 .expect("No test found in declared src?");
 
+            let functions = builtins::prelude_functions(&id_gen);
+
+            let mut data_types = builtins::prelude_data_types(&id_gen);
+
+            for def in ast.definitions() {
+                if let Definition::DataType(dt) = def {
+                    data_types.insert(
+                        DataTypeKey {
+                            module_name: module_name.to_string(),
+                            defined_type: dt.name.clone(),
+                        },
+                        dt.clone(),
+                    );
+                }
+            }
+
             let mut modules = CheckedModules::default();
             modules.insert(
                 module_name.to_string(),
@@ -938,10 +973,6 @@ mod test {
                 },
             );
 
-            let functions = builtins::prelude_functions(&id_gen);
-
-            let data_types = builtins::prelude_data_types(&id_gen);
-
             let mut generator = modules.new_generator(
                 &functions,
                 &data_types,
@@ -949,16 +980,19 @@ mod test {
                 Tracing::All(TraceLevel::Verbose),
             );
 
+            (
                 Self::from_function_definition(
                     &mut generator,
                     test.to_owned(),
                     module_name.to_string(),
                     PathBuf::new(),
+                ),
+                data_types,
             )
         }
     }
 
-    fn property(src: &str) -> PropertyTest {
+    fn property(src: &str) -> (PropertyTest, impl Fn(PlutusData) -> String) {
         let prelude = indoc! { r#"
             use aiken/builtin
 
@@ -999,6 +1033,22 @@ mod test {
               }
             }
 
+            fn bool() -> Fuzzer<Bool> {
+              int() |> map(fn(n) { n % 2 == 0 })
+            }
+
+            fn bytearray() -> Fuzzer<ByteArray> {
+              int()
+                |> map(
+                     fn(n) {
+                       n
+                         |> builtin.integer_to_bytearray(True, 32, _)
+                         |> builtin.blake2b_256()
+                         |> builtin.slice_bytearray(8, 4, _)
+                     },
+                   )
+            }
+
             pub fn constant(a: a) -> Fuzzer<a> {
               fn(s0) { Some((s0, a)) }
             }
@@ -1020,39 +1070,58 @@ mod test {
                 }
               }
             }
+
+            pub fn map2(fuzz_a: Fuzzer<a>, fuzz_b: Fuzzer<b>, f: fn(a, b) -> c) -> Fuzzer<c> {
+              fn(s0) {
+                when fuzz_a(s0) is {
+                  Some((s1, a)) ->
+                    when fuzz_b(s1) is {
+                      Some((s2, b)) -> Some((s2, f(a, b)))
+                      None -> None
+                    }
+                  None -> None
+                }
+              }
+            }
         "#};
 
         let src = format!("{prelude}\n{src}");
 
         match Test::from_source(&src) {
-            Test::PropertyTest(test) => test,
+            (Test::PropertyTest(test), data_types) => {
-            Test::UnitTest(..) => panic!("Expected to yield a PropertyTest but found a UnitTest"),
+                let type_info = test.fuzzer.type_info.clone();
+
+                let reify = move |counterexample| {
+                    let mut data_type_refs = IndexMap::new();
+                    for (k, v) in &data_types {
+                        data_type_refs.insert(k.clone(), v);
+                    }
+
+                    let expr = UntypedExpr::reify(&data_type_refs, counterexample, &type_info)
+                        .expect("Failed to reify value.");
+                    Formatter::new().expr(&expr, false).to_pretty_string(70)
+                };
+
+                (test, reify)
+            }
+            (Test::UnitTest(..), _) => {
+                panic!("Expected to yield a PropertyTest but found a UnitTest")
+            }
         }
     }
 
     impl PropertyTest {
         fn expect_failure(&self, seed: u32) -> Counterexample {
-            let (next_prng, value) = Prng::from_seed(seed)
+            match self.run_n_times(PropertyTest::MAX_TEST_RUN, seed, None) {
-                .sample(&self.fuzzer.program)
+                Some((_, counterexample)) => counterexample,
-                .expect("running seeded Prng cannot fail.");
+                _ => panic!("expected property to fail but it didn't."),
-
-            let result = self.eval(&value);
-
-            if result.failed(self.can_error) {
-                return Counterexample {
-                    value,
-                    choices: next_prng.choices(),
-                    property: self,
-                };
             }
-
-            unreachable!("Prng constructed from a seed necessarily yield a seed.");
         }
     }
 
     #[test]
     fn test_prop_basic() {
-        let prop = property(indoc! { r#"
+        let (prop, _) = property(indoc! { r#"
             test foo(n: Int via int()) {
                 n >= 0
             }
@@ -1063,16 +1132,249 @@ mod test {
 
     #[test]
     fn test_prop_always_odd() {
-        let prop = property(indoc! { r#"
+        let (prop, reify) = property(indoc! { r#"
             test foo(n: Int via int()) {
                 n % 2 == 0
             }
         "#});
 
-        let mut counterexample = prop.expect_failure(12);
+        let mut counterexample = prop.expect_failure(42);
 
         counterexample.simplify();
 
         assert_eq!(counterexample.choices, vec![1]);
+        assert_eq!(reify(counterexample.value), "1");
+    }
+
+    #[test]
+    fn test_prop_combine() {
+        let (prop, reify) = property(indoc! { r#"
+            fn pair(fuzz_a: Fuzzer<a>, fuzz_b: Fuzzer<b>) -> Fuzzer<(a, b)> {
+                fuzz_a
+                    |> and_then(fn(a) {
+                        fuzz_b
+                            |> map(fn(b) {
+                                (a, b)
+                            })
+                    })
+            }
+
+
+            test foo(t: (Int, Int) via pair(int(), int())) {
+                t.1st + t.2nd <= 400
+            }
+        "#});
+
+        let mut counterexample = prop.expect_failure(42);
+
+        counterexample.simplify();
+
+        assert_eq!(counterexample.choices, vec![201, 200]);
+        assert_eq!(reify(counterexample.value), "(201, 200)");
+    }
+
+    #[test]
+    fn test_prop_enum_bool() {
+        let (prop, reify) = property(indoc! { r#"
+            test foo(predicate via bool()) {
+                predicate
+            }
+        "#});
+
+        let mut counterexample = prop.expect_failure(42);
+
+        counterexample.simplify();
+
+        assert_eq!(counterexample.choices, vec![1]);
+        assert_eq!(reify(counterexample.value), "False");
+    }
+
+    #[test]
+    fn test_prop_enum_custom() {
+        let (prop, reify) = property(indoc! { r#"
+            type Temperature {
+                Hot
+                Cold
+            }
+
+            fn temperature() -> Fuzzer<Temperature> {
+                bool() |> map(fn(is_cold) {
+                    if is_cold { Cold } else { Hot }
+                })
+            }
+
+            test foo(t via temperature()) {
+                t == Hot
+            }
+        "#});
+
+        let mut counterexample = prop.expect_failure(42);
+
+        counterexample.simplify();
+
+        assert_eq!(counterexample.choices, vec![0]);
+        assert_eq!(reify(counterexample.value), "Cold");
+    }
+
+    #[test]
+    fn test_prop_opaque() {
+        let (prop, reify) = property(indoc! { r#"
+            opaque type Temperature {
+                Hot
+                Cold
+            }
+
+            fn temperature() -> Fuzzer<Temperature> {
+                bool() |> map(fn(is_cold) {
+                    if is_cold { Cold } else { Hot }
+                })
+            }
+
+            test foo(t via temperature()) {
+                t == Hot
+            }
+        "#});
+
+        let mut counterexample = prop.expect_failure(42);
+
+        counterexample.simplify();
+
+        assert_eq!(counterexample.choices, vec![0]);
+        assert_eq!(reify(counterexample.value), "Cold");
+    }
+
+    #[test]
+    fn test_prop_private_enum() {
+        let (prop, reify) = property(indoc! { r#"
+            type Vehicle {
+                Car { wheels: Int }
+                Bike { wheels: Int }
+            }
+
+            fn vehicle() -> Fuzzer<Vehicle> {
+                bool() |> map(fn(is_car) {
+                    if is_car { Car(4) } else { Bike(2) }
+                })
+            }
+
+            test foo(v via vehicle()) {
+                when v is {
+                    Car { wheels } -> wheels
+                    Bike { wheels } -> wheels
+                } == 4
+            }
+        "#});
+
+        let mut counterexample = prop.expect_failure(42);
+
+        counterexample.simplify();
+
+        assert_eq!(counterexample.choices, vec![1]);
+        assert_eq!(reify(counterexample.value), "Bike { wheels: 2 }");
+    }
+
+    #[test]
+    fn test_prop_list() {
+        let (prop, reify) = property(indoc! { r#"
+            fn list(elem: Fuzzer<a>) -> Fuzzer<List<a>> {
+              bool()
+                |> and_then(fn(continue) {
+                    if continue {
+                      map2(elem, list(elem), fn(head, tail) { [head, ..tail] })
+                    } else {
+                      constant([])
+                    }
+                })
+            }
+
+            fn length(es: List<a>) -> Int {
+              when es is {
+                [] -> 0
+                [_, ..tail] -> 1 + length(tail)
+              }
+            }
+
+            test foo(es: List<Int> via list(int())) {
+              length(es) < 3
+            }
+        "#});
+
+        let mut counterexample = prop.expect_failure(42);
+
+        counterexample.simplify();
+
+        assert_eq!(counterexample.choices, vec![0, 0, 0, 0, 0, 0, 1]);
+        assert_eq!(reify(counterexample.value), "[0, 0, 0]");
+    }
+
+    #[test]
+    fn test_prop_opaque_dict() {
+        let (prop, reify) = property(indoc! { r#"
+            pub opaque type Dict<a> {
+              inner: List<(ByteArray, a)>,
+            }
+
+            fn dict(elem: Fuzzer<a>) -> Fuzzer<Dict<a>> {
+              bool()
+                |> and_then(
+                     fn(continue) {
+                       if continue {
+                         let kv = map2(bytearray(), elem, fn(k, v) { (k, v) })
+                         map2(kv, dict(elem), fn(head, tail) { Dict([head, ..tail.inner]) })
+                       } else {
+                         constant(Dict([]))
+                       }
+                     },
+                   )
+            }
+
+            test foo(d via dict(bool())) {
+              d == Dict([])
+            }
+        "#});
+
+        let mut counterexample = prop.expect_failure(42);
+
+        counterexample.simplify();
+
+        assert_eq!(counterexample.choices, vec![0, 0, 0, 1]);
+        assert_eq!(reify(counterexample.value), "Dict([(#\"2cd15ed0\", True)])");
+    }
+
+    #[test]
+    fn test_prop_opaque_nested_dict() {
+        let (prop, reify) = property(indoc! { r#"
+            pub opaque type Dict<a> {
+              inner: List<(ByteArray, a)>,
+            }
+
+            fn dict(elem: Fuzzer<a>) -> Fuzzer<Dict<a>> {
+              bool()
+                |> and_then(
+                     fn(continue) {
+                       if continue {
+                         let kv = map2(bytearray(), elem, fn(k, v) { (k, v) })
+                         map2(kv, dict(elem), fn(head, tail) { Dict([head, ..tail.inner]) })
+                       } else {
+                         constant(Dict([]))
+                       }
+                     },
+                   )
+            }
+
+            test foo(d via dict(dict(int()))) {
+              d == Dict([])
+            }
+        "#});
+
+        let mut counterexample = prop.expect_failure(42);
+
+        counterexample.simplify();
+
+        assert_eq!(counterexample.choices, vec![0, 0, 1, 1]);
+        assert_eq!(
+            reify(counterexample.value),
+            "Dict([(#\"2cd15ed0\", Dict([]))])"
+        );
     }
 }