[ check ] Fix type-checking bug, add more example

CHANGELOG.md

@@ -3,6 +3,8 @@
 # 0.1.6
 
 + Integrate `minitt-util` for CLI
++ Fix type-checking bug
++ Fix reduction bug
 
 # 0.1.5
 

samples/row-polymorphism/extensible-pattern-match.out

@@ -0,0 +1,20 @@
+Parse successful.
+sign: set1
+body: Rec {}
+sign: set1
+body: Sum {}
+sign: Rec {}
+body: {||}
+sign: set1
+body: Sum {False: Rec {}, True: Rec {}}
+sign: Sum {False: Rec {}, True: Rec {}}
+body: (@True {||})
+sign: Sum {False: Rec {}, True: Rec {}}
+body: (@False {||})
+sign: ((Sum {False: Rec {}} -> Sum {False: Rec {}, True: Rec {}}) -> (Sum {False: Rec {}, True: Rec {}} -> Sum {False: Rec {}, True: Rec {}}))
+body: (\ (cases {{ True: \ (\ (@False {||})); } or [0]))
+sign: ((Sum {} -> Sum {False: Rec {}, True: Rec {}}) -> (Sum {False: Rec {}} -> Sum {False: Rec {}, True: Rec {}}))
+body: (\ (cases {{ False: \ (\ (@True {||})); } or [0]))
+sign: (Sum {False: Rec {}, True: Rec {}} -> Sum {False: Rec {}, True: Rec {}})
+body: (\ False => (\ (@True {||})); True => (\ (@False {||})); )
+Checkmate, dram!

samples/row-polymorphism/extensible-pattern-match.voile

@@ -0,0 +1,30 @@
+//
+// Created by Dependently-Typed Lambda Calculus on 2019-08-29
+// simple-pattern-match
+// Author: ice10
+//
+
+let Unit = Rec {};
+let Bottom = Sum {};
+
+val unit : Unit;
+let unit = {| |};
+
+let Bool = Sum { True: Unit; False: Unit; };
+
+val true : Bool;
+let true = @True unit;
+
+val false : Bool;
+let false = @False unit;
+
+val notTrue : (Sum { False: Unit; } -> Bool)
+            -> Bool -> Bool;
+let notTrue = \f. case True u: false or f;
+
+val notFalse : (Bottom -> Bool)
+             -> Sum { False: Unit; } -> Bool;
+let notFalse = \f. case False u: true or f;
+
+val not : Bool -> Bool;
+let not = notTrue (notFalse whatever);

src/check/expr.rs

@@ -230,7 +230,7 @@ fn check(mut tcs: TCS, expr: &Abs, expected_type: &Val) -> ValTCM {
             Val::RowPoly(Variant, variants) if variants.is_empty() => {
                 Ok((Val::Lam(Closure::default()).into_info(*info), tcs))
             }
-            ty => Err(TCE::NotRowType(Variant, (*info).clone(), ty.clone())),
+            ty => Err(TCE::NotEmpty(info.clone(), ty.clone())),
         },
         // How about when `Dt` is `Plicit::Im`?
         (CaseOr(label, binding, uid, body, or), Val::Dt(Pi, Plicit::Ex, param_ty, ret_ty)) => {

src/check/monad/error.rs

@@ -26,6 +26,7 @@ pub enum TCE {
     NotTypeAbs(Loc, Abs),
     NotTypeVal(Loc, Val),
     NotRowType(VarRec, Loc, Val),
+    NotEmpty(Loc, Val),
     NotRecVal(Loc, Val),
     NotUniverseVal(Loc, Val),
 
@@ -107,6 +108,11 @@ impl Display for TCE {
                 "Expected a variant type expression, got: `{}` at {}.",
                 val, id
             ),
+            TCE::NotEmpty(id, val) => write!(
+                f,
+                "Expected an empty type expression, got: `{}` at {}.",
+                val, id
+            ),
             TCE::MissingVariant(VarRec::Variant, variant) => {
                 write!(f, "Missing variant `{}`.", variant)
             }