[ #7 ] Negative examples

samples/negative/girard-paradox.minitt

@@ -0,0 +1,7 @@
+--
+-- Created by intellij-minitt on 2019-03-16
+-- girard-paradox
+-- Author: ice1000
+--
+
+let error: Type = Type;

samples/negative/girard-paradox.out

@@ -0,0 +1,5 @@
+Parse successful.
+Type mismatch: expected `Type0`, got (inferred): `Type1`.
+When checking the declaration of `error`.
+thread 'main' panicked at 'Type-Check failed.: ()', src/libcore/result.rs:997:5
+note: Run with `RUST_BACKTRACE=1` environment variable to display a backtrace.

samples/test.pl

@@ -39,7 +39,7 @@
             map {say red("  $_")} split /\n/, $diff;
             next if $isCI;
             print colored('  Update the golden value (y/N)? ', 'cyan');
-            (readline =~ s/[\n\r]//rg) eq 'y' ? `$cmd > $out`
+            (readline =~ s/[\n\r]//rg) eq 'y' ? `$cmd > $out 2>&1`
                 : say colored(<<"HINT", 'bold yellow');
   Leaving it alone.
   To update the golden value, run `test_runner.pl` in `src/test` directly.

src/check/decl.rs

@@ -30,6 +30,7 @@ pub fn check_lift_parameters<'a>(
         return check_body(tcs);
     }
     let (pattern, expression) = parameters.remove(0);
+    // TODO: this level might be the pi level
     let (_level, TCS { gamma, context }) = check_type(index, tcs, *expression.clone())?;
     let generated = generate_value(index);
     let type_val = expression.clone().eval(context.clone());
@@ -130,6 +131,7 @@ pub fn check_declaration(index: u32, tcs: TCS, declaration: Declaration) -> TCM<
             body,
             declaration_type: Simple,
         } => check_lift_parameters(index, tcs_borrow!(tcs), prefix_parameters, |tcs| {
+            // TODO: this level might be the pi level
             let (_level, tcs) = check_type(index, tcs, signature.clone())
                 .map_err(|err| try_locate!(err, pattern))?;
             let context = tcs.context();
@@ -145,6 +147,7 @@ pub fn check_declaration(index: u32, tcs: TCS, declaration: Declaration) -> TCM<
                 tcs_borrow!(tcs),
                 declaration.prefix_parameters.clone(),
                 |tcs| {
+                    // TODO: this level might be the pi level
                     let (_level, TCS { gamma, context }) =
                         check_type(index, tcs, declaration.signature.clone())
                             .map_err(|err| try_locate!(err, pattern))?;