collapse unreachable cases to whatever

now, when Kind can detect that a case is definitely unreachable, you can
fill it with whatever (any value). example:

IsTrue
: ∀(b: B/Bool)
  *
= λb #[b]{
  #Indeed{} : (IsTrue #True)
}

Main
: ∀(x: B/Bool)
  ∀(t: (IsTrue x))
  B/Bool
= λ{
  #True: λ{
    #Indeed: #True{}
  }
  #False: λ{
    #Indeed: 0
  }
}

here, since we can detect that the False case is unreachable, we change
its goal to a hole, letting the user type anything.

src/Kind/Check.hs

@@ -183,7 +183,10 @@ check src val typ dep = debug ("check: " ++ termShower True val dep ++ "\n    ::
                   let eqs = extractEqualities (reduce book fill 2 typ_inp) (reduce book fill 2 (snd a_r)) dep
                   let rt0 = teleToType tele (typ_bod (Ann False (Con cnm (fst a_r)) typ_inp)) dep
                   let rt1 = foldl' (\ ty (a,b) -> replace a b ty dep) rt0 eqs
-                  check Nothing cbod rt1 dep
+                  if any (\(a,b) -> incompatible a b dep) eqs then
+                    check Nothing cbod (Hol "unreachable" []) dep
+                  else
+                    check Nothing cbod rt1 dep
                 Nothing -> do
                   envLog (Error src (Hol ("constructor_not_found:"++cnm) []) (Hol "unknown_type" []) (Mat cse) dep)
                   envFail
@@ -303,10 +306,7 @@ teleToTerm tele dep = go tele [] dep where
 
 extractEqualities :: Term -> Term -> Int -> [(Term, Term)]
 extractEqualities (Dat as _) (Dat bs _) dep = zip as bs where
-  -- go (Var _ i) v = (i, v)
-  -- go (Src _ i) v = go i v
-  -- go a         v = trace ("Unexpected term: " ++ termShower True a dep ++ " == " ++ termShower True v dep) (0, v)
-extractEqualities a b dep = trace ("Unexpected terms: " ++ termShower True a dep ++ " and " ++ termShower True b dep) []
+extractEqualities a          b          dep = trace ("Unexpected terms: " ++ termShower True a dep ++ " and " ++ termShower True b dep) []
 
 doCheck :: Term -> Env ()
 doCheck (Ann _ val typ) = check Nothing val typ 0 >> return ()

src/Kind/Equal.hs

@@ -485,3 +485,13 @@ replace old neo term dep = if same old term dep then neo else go term where
   goCse (cnam, cbod)    = (cnam, replace old neo cbod dep)
   goTele (TRet term)  d = TRet (replace old neo term d)
   goTele (TExt k t b) d = TExt k (replace old neo t d) (\x -> goTele (b x) (d+1))
+
+-- Returns true when two terms can definitely never be made identical.
+-- TODO: to implement this, just recurse pairwise on the Con constructor,
+-- until a different name is found. All other terms are considered compatible.
+incompatible :: Term -> Term -> Int -> Bool
+incompatible (Con aNam aArg) (Con bNam bArg) dep | aNam /= bNam = True
+incompatible (Con aNam aArg) (Con bNam bArg) dep | otherwise    = length aArg == length bArg && any (\(a,b) -> incompatible a b dep) (zip (map snd aArg) (map snd bArg))
+incompatible (Src aSrc aVal) b               dep                = incompatible aVal b dep
+incompatible a               (Src bSrc bVal) dep                = incompatible a bVal dep
+incompatible _               _               _                  = False