Drop incompatible constructors in case

TODO.md

@@ -3,6 +3,9 @@
 
 I may be done with `U` - I keep typing `Type`.
 
+- [ ] eval for case (see order.newt)
+- [ ] fix `ite.newt`
+- [ ] dynamic pattern unification (add test case first)
 - [x] switch from commit/mustWork to checking progress
 - [x] type constructors are no longer generated?  And seem to have 0 arity.
 - [x] raw let is not yet implemented (although define used by case tree building)

newt/order.newt

@@ -0,0 +1,29 @@
+module Order
+
+data Nat : U where
+  Z : Nat
+  S : Nat -> Nat
+
+plus : Nat -> Nat -> Nat
+plus Z y = y
+plus (S x) y = S (plus x y)
+
+data Pair : U -> U -> U where
+  _,_ : {A B : U} -> A -> B -> Pair A B
+
+infix 1 _,_
+
+foo : Pair Nat Nat
+foo = (Z , S Z)
+
+-- So I was going to force a (a + b, a) =?= (3,0) unification problem
+-- as an example of needing _dynamic_ pattern unification
+data Eq : {A : U} -> A -> A -> U where
+  Refl : {A : U} -> {x : A} -> Eq x x
+
+-- but hold up here.  This doesn't solve either.
+-- Oh, because I can't reduce case.
+-- And the FC is useless.
+two : Eq (plus Z (S (S Z))) (S (S Z))
+two = Refl {Nat} {S (S Z)}
+

newt/typeclass.newt

@@ -4,6 +4,13 @@ module TypeClass
 
 -- this would be nicer with records and copatterns
 
+-- At this point, for Agda style, I'll probably need to postpone, or collect constraints
+-- at lesat. Idris style, I might get away without short term.
+
+-- So I can read mcbride paper and maybe agda source.
+
+
+
 -- we need a bit more than this, but
 data Monad : (U -> U) -> U where
   MkMonad : { M : U -> U } ->
@@ -15,6 +22,17 @@ data Maybe : U -> U where
   Nothing : {A : U} -> Maybe A
 
 
+data Either : U -> U -> U where
+  Left : {A B : U} -> A -> Either A B
+  Right : {A B : U} -> B -> Either A B
+
+EitherMonad : {A : U} -> Monad (Either A)
+EitherMonad = MkMonad {Either A} (\ ma amb =>
+--                     ^ Need this for scrut type to be non-meta
+  case ma of
+    Left a => Left a
+    Right b => amb b)
+
 -- [instance]
 MaybeMonad : Monad Maybe
 -- Agda case lambda might be nice..
@@ -44,5 +62,29 @@ ptype Int
 -- Idris gets this by specially treating determining arguments of an auto as "invertible". It then unifies
 -- the last arg on each side and tries the rest, which is now in the pattern fragment.
 
+-- Agda may do this slightly differently from Idris:
+--    https://agda.readthedocs.io/en/v2.6.0.1/language/instance-arguments.html#instance-resolution
+
+-- I think it searches, pulls in all possibilities and tries to unify them into place.
+-- We'll want to extend our example to what I have in Foo2.agda to test that it finds the right
+-- one. Maybe look at the source to see if there is any invertible trickery going on?
+
+-- I know that here, if I fill in the instance, everything works out, so finding the instance that works
+-- out might be sufficient.  That might mean that a instance constraint is a pile of options that get
+-- winnowed down?
+
+-- Putting MaybeMonad in there helps the unification
+-- of Maybe Int =?= ?m6 ?m2 (as Monad Maybe (the type) gives ?m6 is Maybe)
+-- and MaybeEither would fail after a couple of steps. But it seems expensive/complex
+-- to have to run the process down for each candidate.
+
+-- Agda seems complicated, minting fresh metas for bits of potential solutions (which
+-- may be tossed if the solution is ruled out.)
+
 foo : Int -> Maybe Int
-foo x = _>>=_ (Just x) (\ x  => Just 10)
+foo x = _>>=_ {_} {_} {_} {_} (Just x) (\ x  => Just 10)
+--                         ^
+/-
+So, agda style we'd guess ?m8 is MonadMaybe or MonadEither - agda's "maybe" case
+
+-/

src/Lib/Check.idr

@@ -19,7 +19,7 @@ import Lib.Syntax
 data Pden = PR Nat Nat (List Nat)
 
 -- IORef for metas needs IO
-
+export
 forceMeta : Val -> M Val
 forceMeta (VMeta fc ix sp) = case !(lookupMeta ix) of
   (Unsolved pos k xs _) => pure (VMeta fc ix sp)
@@ -102,7 +102,7 @@ parameters (ctx: Context)
 
   solve : Nat -> Nat -> SnocList Val -> Val  -> M  ()
   solve l m sp t = do
-    debug "solve \{show l} \{show m} \{show sp} \{show t}"
+    debug "solve \{show m} lvl \{show l} sp \{show sp} is \{show t}"
     meta <- lookupMeta m
     debug "meta \{show meta}"
     ren <- invert l sp
@@ -113,6 +113,13 @@ parameters (ctx: Context)
     solveMeta top m soln
     pure ()
 
+  trySolve : Nat -> Nat -> SnocList Val -> Val -> M ()
+  trySolve l m sp t = do
+    catchError {e=Error} (solve l m sp t) $ (\err => do
+      debug $ showError "" err
+      pure ())
+
+
   export
   unify : (l : Nat) -> Val -> Val  -> M UnifyResult
 
@@ -160,9 +167,9 @@ parameters (ctx: Context)
       (VMeta fc k sp,  VMeta fc' k' sp' ) =>
         if k == k' then unifySpine l (k == k') sp sp'
         -- TODO, might want to try the other way, too.
-        else solve l k sp (VMeta fc' k' sp') >> pure neutral
+        else trySolve l k sp (VMeta fc' k' sp') >> pure neutral
-      (t,           VMeta fc' i' sp') => solve l i' sp' t >> pure neutral
+      (t,           VMeta fc' i' sp') => trySolve l i' sp' t >> pure neutral
-      (VMeta fc i sp, t'           ) => solve l i sp t' >> pure neutral
+      (VMeta fc i sp, t'           ) => trySolve l i sp t' >> pure neutral
       (VPi fc _ _ a b, VPi fc' _ _ a' b') => [| unify l a a' <+> unify (S l) !(b $$ VVar emptyFC l [<]) !(b' $$ VVar emptyFC l [<]) |]
       (VVar fc k sp,   (VVar fc' k' sp')  ) =>
         if k == k' then unifySpine l (k == k') sp sp'
@@ -177,8 +184,7 @@ parameters (ctx: Context)
         if k == k' then do
           debug "unify \{show l} spine at \{k} \{show sp} \{show sp'}"
           unifySpine l (k == k') sp sp'
-        -- REVIEW - consider forcing?
+        else error fc "vref mismatch \{show k} \{show k'} -- \{show sp} \{show sp'}"
-        else error emptyFC "vref mismatch \{show k} \{show k'} -- \{show sp} \{show sp'}"
 
       (VU _, VU _) => pure neutral
       -- Lennart.newt cursed type references itself
@@ -343,7 +349,8 @@ updateContext ctx ((k, val) :: cs) = let ix = (length ctx.env `minus` k) `minus`
 -- ok, so this is a single constructor, CaseAlt
 -- since we've gotten here, we assume it's possible and we better have at least
 -- one valid clause
-buildCase : Context -> Problem -> String -> Val -> (String, Nat, Tm) -> M CaseAlt
+-- return Nothing if dcon doesn't unify with scrut
+buildCase : Context -> Problem -> String -> Val -> (String, Nat, Tm) -> M (Maybe CaseAlt)
 buildCase ctx prob scnm scty (dcName, arity, ty) = do
   debug "CASE \{scnm} \{dcName} \{pprint (names ctx) ty}"
   vty <- eval [] CBN ty
@@ -359,7 +366,8 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
   -- We get unification constraints from matching the data constructors
   -- codomain with the scrutinee type
   debug "unify dcon dom with scrut"
-  res <- unify ctx' (length ctx'.env) ty' scty
+  Just res <- catchError {e = Error} (Just <$> unify ctx' (length ctx'.env) ty' scty) (\_ => pure Nothing)
+    | _ => pure Nothing
 
   -- Additionally, we constrain the scrutinee's variable to be
   -- dcon applied to args
@@ -397,7 +405,7 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
 
   when (length clauses == 0) $ error ctx.fc "Missing case for \{dcName} splitting \{scnm}"
   tm <- buildTree ctx' (MkProb clauses prob.ty)
-  pure $ CaseCons dcName (map getName vars) tm
+  pure $ Just $ CaseCons dcName (map getName vars) tm
   where
     getName : Bind -> String
     getName (MkBind nm _ _) = nm
@@ -528,7 +536,8 @@ buildTree ctx prob@(MkProb ((MkClause fc constraints [] expr) :: cs) ty) = do
   cons <- getConstructors ctx scty
   alts <- traverse (buildCase ctx prob scnm scty) cons
 
-  pure $ Case fc sctm alts
+  -- TODO check for empty somewhere?
+  pure $ Case fc sctm (catMaybes alts)
 
 
 showDef : Context -> List String -> Nat -> Val -> M String
@@ -554,7 +563,7 @@ check ctx tm ty = case (tm, !(forceType ty)) of
     let ctx' = extend ctx scnm scty
     cons <- getConstructors ctx' scty
     alts <- traverse (buildCase ctx' (MkProb clauses ty) scnm scty) cons
-    pure $ Let fc scnm sc $ Case fc (Bnd fc 0) alts
+    pure $ Let fc scnm sc $ Case fc (Bnd fc 0) (catMaybes alts)
 
   -- Document a hole, pretend it's implemented
   (RHole fc, ty) => do

src/Lib/Parser.idr

@@ -95,8 +95,8 @@ parseOp = parseApp >>= go 0
     go : Int -> Raw -> Parser Raw
     go prec left =
       try (do
-        op <- token Oper
         fc <- getPos
+        op <- token Oper
         ops <- getOps
         let op' = "_" ++ op ++ "_"
         let Just (p,fix) = lookup op' ops

src/Lib/ProcessDecl.idr

@@ -82,12 +82,15 @@ processDecl (Def fc nm clauses) = do
 
   for_ mc.metas $ \case
     (Solved k x) => pure ()
-    (Unsolved (l,c) k xs ty) => do
+    (Unsolved (l,c) k ctx ty) => do
       -- should just print, but it's too subtle in the sea of messages
       -- we'd also need the ability to mark the whole top context as failure if we continue
       -- put a list of errors in TopContext
-      putStrLn $ showError "" $ E (l,c) "Unsolved meta \{show k}"
+
-      addError $ E (l,c) "Unsolved meta \{show k}"
+      -- Something wrong here - bad VVar
+      tm <- quote ctx.lvl !(forceMeta ty)
+      -- putStrLn $ showError "" $ E (l,c) "Unsolved meta \{show k} type \{show ty}"
+      addError $ E (l,c) "Unsolved meta \{show k} type \{pprint (names ctx) tm}"
       -- throwError $ E (l,c) "Unsolved meta \{show k}"
   debug "Add def \{nm} \{pprint [] tm'} : \{pprint [] ty}"
   modify $ setDef nm ty (Fn tm')

tests/black/case3.newt

@@ -0,0 +1,18 @@
+module Case3
+
+data Nat : U where
+  Z : Nat
+  S : Nat -> Nat
+
+data Vect : Nat -> U -> U where
+  Nil : {a : U} -> Vect Z a
+  _::_ : {a : U} -> {k : Nat} -> a -> Vect k a -> Vect (S k) a
+
+infixr 5 _::_
+
+head : {a : U} {k : Nat} -> Vect (S k) a -> a
+head (x :: xs) = x
+
+zapp : {s t: U} {k : Nat} -> Vect k (s -> t) -> Vect k s -> Vect k t
+zapp (f :: fs) (t :: ts) = f t :: zapp fs ts
+zapp Nil Nil = Nil