fix: False positive in type equality

brat/Brat/Checker/SolveHoles.hs

@@ -83,8 +83,11 @@ typeEqEta tm stuff@(ny :* _ks :* _sems) hopes k exp act = do
   when (or [M.member ie hopes | InEnd ie <- ends]) $ typeErr "ends were in hopeset"
   case ends of
     [] -> typeEqRigid tm stuff k exp act -- easyish, both rigid i.e. already defined
-    [e1, e2] | e1 == e2 -> pure () -- trivially same, even if both still yet-to-be-defined
-    _es -> error "TODO: must wait for one or the other to become more defined"
+    -- variables are trivially the same, even if undefined, but the values may
+    -- be different! E.g. X =? 1 + X
+    [_, _] | exp == act -> pure ()
+    -- TODO: Once we have scheduling, we must wait for one or the other to become more defined, rather than failing
+    _  -> err (TypeMismatch tm (show exp) (show act))
  where
   getEnd (VApp (VPar e) _) = Just e
   getEnd (VNum n) = getNumVar n

brat/Brat/Syntax/Value.hs

@@ -33,7 +33,8 @@ import Hasochism
 import Data.List (intercalate, minimumBy)
 import Data.Ord (comparing)
 import Data.Kind (Type)
-import Data.Type.Equality ((:~:)(..))
+import Data.Maybe (isJust)
+import Data.Type.Equality ((:~:)(..), testEquality)
 
 newtype VDecl = VDecl (FuncDecl (Some (Ro Brat Z)) (FunBody Term Noun))
 
@@ -159,6 +160,31 @@ data Val :: N -> Type where
   VApp :: VVar n -> Bwd (Val n) -> Val n
   VSum :: MODEY m => Modey m -> [Some (Ro m n)] -> Val n -- (Hugr-like) Sum types
 
+-- Define a naive version of equality, which only says whether the data
+-- structures are on-the-node equal
+instance Eq (Val n) where
+  VNum a == VNum b = a == b
+  (VCon c xs) == (VCon d ys) = c == d && xs == ys
+  (VLam x) == (VLam y) = x == y
+  (VFun m cty) == (VFun m' cty') = case testEquality m m' of
+    Just Refl -> cty == cty'
+    Nothing -> False
+  (VApp v zx) == (VApp w zy) = v == w && zx == zy
+  _ == _ =  False
+
+instance MODEY m => Eq (CTy m i) where
+  (ss :->> ts) == (us :->> vs) = case roEq (modey @m) ss us of
+                                   Just Refl -> isJust (roEq (modey @m) ts vs)
+                                   Nothing -> False
+   where
+    roEq :: forall m i j k. Modey m -> Ro m i j -> Ro m i k -> Maybe (j :~: k)
+    roEq _ R0 R0 = Just Refl
+    roEq my (RPr x ro) (RPr y rp) | x == y = roEq my ro rp
+    roEq Braty (REx x ro) (REx y rp) | x == y = case roEq Braty ro rp of
+      Just Refl -> Just Refl
+      Nothing -> Nothing
+    roEq _ _ _ = Nothing
+
 data SVar = SPar End | SLvl Int
  deriving (Show, Eq)
 

brat/test/golden/error/vec_length.brat

@@ -0,0 +1,2 @@
+f(X :: *, n :: #, Vec(X, 1 + n)) -> Vec(X, n)
+f(_, _, xs) = xs

brat/test/golden/error/vec_length.brat.golden

@@ -0,0 +1,9 @@
+Error in test/golden/error/vec_length.brat on line 2:
+f(_, _, xs) = xs
+              ^^
+
+  Type mismatch when checking xs
+Expected: (a1 :: Vec(VApp VPar Ex checking_check_defs_1_f_f.box_2_lambda_fake_source 0 B0, VPar Ex checking_check_defs_1_f_f.box_2_lambda_fake_source 1))
+But got:  (xs :: Vec(VApp VPar Ex checking_check_defs_1_f_f.box_2_lambda_fake_source 0 B0, 1 + VPar Ex checking_check_defs_1_f_f.box_2_lambda_fake_source 1))
+
+