Slight improvement to a broken system

brat/Brat/Checker.hs

@@ -798,9 +798,9 @@ detectVecErrors :: UserName  -- Term constructor name
                 -> Checking (Error -> Error)  -- Returns error wrapper to use for recursion
 detectVecErrors vcon (PrefixName [] "Vec") [_, VNum n] [_, VPNum p] ty tp =
   case numMatch B0 n p of
-    Left (NumMatchFail _ _) -> do
-      p' <- toLenConstr p
-      err $ getVecErr tp (show ty) (show n) p'
+    Left (NumMatchFail _ _) -> case (toLenConstr p) of
+      Right p' -> err $ getVecErr tp (show ty) (show n) p'
+      Left p' -> err $ InternalError ("detectVecErrors: Unexpected pattern: " ++ show (toLenConstr p'))
     -- Even if we succed here, the error might pop up when checking the
     -- rest of the vector. We return a function here that intercepts the
     -- error and extends it to the whole vector.
@@ -809,13 +809,14 @@ detectVecErrors vcon (PrefixName [] "Vec") [_, VNum n] [_, VPNum p] ty tp =
                  pure (consError fc tp (show ty) n)
          else pure id
  where
-  -- For constructors that produce something of type Vec we should
-  -- only ever get the patterns NP0 (if vcon == PrefixName [] "nil")
-  -- and NP1Plus (if vcon == PrefixName [] "cons")
-  toLenConstr :: NumPat -> Checking LengthConstraint
+  -- Try to work out the length of a vector
+  -- We only want to know if the vector length is nil or a successor
+  toLenConstr :: NumPat -> Either NumPat (LengthConstraint)
   toLenConstr NP0 = pure $ Length 0
+  toLenConstr (NP1Plus (NP2Times np)) = either (const (Right LengthOdd)) Right (toLenConstr np)
   toLenConstr (NP1Plus _) = pure $ LongerThan 0
-  toLenConstr p = err $ InternalError ("detectVecErrors: Unexpected pattern: " ++ show p)
+  toLenConstr (NP2Times np) = either (const (Right LengthEven)) Right (toLenConstr np)
+  toLenConstr p = Left p
 detectVecErrors _ _ _ _ _ _ = pure id
 
 getVecErr :: Either (Term d k) Pattern -> (String -> String -> LengthConstraint -> ErrorMsg)

brat/Brat/Error.hs

@@ -18,10 +18,12 @@ newtype ParseError = PE { pretty :: String }
 instance Show ParseError where
   show = pretty
 
-data LengthConstraintF a = Length a | LongerThan a deriving (Eq, Functor)
+data LengthConstraintF a = Length a | LongerThan a | LengthEven | LengthOdd deriving (Eq, Functor)
 instance Show a => Show (LengthConstraintF a) where
-  show (Length a) = show a
-  show (LongerThan a) = "(> " ++ show a ++ ")"
+  show (Length a) = "of length " ++ show a
+  show (LongerThan a) = "with length (> " ++ show a ++ ")"
+  show LengthEven = "of even length"
+  show LengthOdd = "of odd length"
 
 type LengthConstraint = LengthConstraintF Int
 
@@ -102,12 +104,12 @@ instance Show ErrorMsg where
   show (VecLength tm ty exp act) = unlines ["Expected vector of length " ++ exp
                                        ,"from the type:  " ++ ty
                                        ,"but got vector: " ++ tm
-                                       ,"of length " ++ show act
+                                       ,show act
                                        ]
   show (VecPatLength abs ty exp act) = unlines ["Pattern: " ++ abs
                                        ,"doesn't match type " ++ ty
                                        ,"(expected vector pattern of length " ++ exp ++
-                                        " but got vector pattern of length " ++ show act ++ ")"
+                                        " but got vector pattern " ++ show act ++ ")"
                                        ]
   show (NotVecPat tm ty)= unwords ["Expected", tm
                                   ,"to be a vector pattern when binding type", ty]

brat/test/Test/Compile/Hugr.hs

@@ -60,7 +60,8 @@ nonCompilingExamples = (expectedCheckingFails ++ expectedParsingFails ++
   -- Conjecture: These examples don't compile because number patterns in type
   -- signatures causes `kindCheck` to call `abstract`, creating "Selector"
   -- nodes, which we don't attempt to compile because we want to get rid of them
-  ,"vec-pats"
+  ,"brick" -- Creates Selectors
+
   -- Victims of #389
   ,"arith"
   ,"bell"

brat/test/golden/error/badvec3.brat.golden

@@ -5,6 +5,6 @@ v3 = cons(1, nil)
   Expected vector of length 0
 from the type:  Vec(Int, 0)
 but got vector: [1]
-of length (> 0)
+with length (> 0)
 
 

brat/test/golden/error/even-length.brat

@@ -0,0 +1,5 @@
+f(X :: *, n :: #, Vec(X, n)) -> Vec(X, n)
+f(X, n, xs) = xs
+
+g :: Vec(Nat, 3)
+g = f(Nat, 3, [1] =,= [2])

brat/test/golden/error/even-length.brat.golden

@@ -0,0 +1,10 @@
+Error in test/golden/error/even-length.brat@FC {start = Pos {line = 5, col = 15}, end = Pos {line = 5, col = 26}}:
+g = f(Nat, 3, [1] =,= [2])
+              ^^^^^^^^^^^
+
+  Expected vector of length 3
+from the type:  Vec(VApp VPar In checking_check_defs_1_g_1_ 0 B0, VPar In checking_check_defs_1_g_1_ 1)
+but got vector: concatEqEven([1], [2])
+of even length
+
+

brat/test/golden/error/kbadvec3.brat.golden

@@ -5,6 +5,6 @@ constNil = { b => cons(1, nil) }
   Expected vector of length 0
 from the type:  Vec(Bit, 0)
 but got vector: [1]
-of length (> 0)
+with length (> 0)
 
 

brat/test/golden/error/odd-length.brat

@@ -0,0 +1,5 @@
+f(X :: *, n :: #, Vec(X, n)) -> Vec(X, n)
+f(X, n, xs) = xs
+
+g :: Vec(Nat, 4)
+g = f(Nat, 4, [1] =, 2 ,= [3])

brat/test/golden/error/odd-length.brat.golden

@@ -0,0 +1,10 @@
+Error in test/golden/error/odd-length.brat@FC {start = Pos {line = 5, col = 15}, end = Pos {line = 5, col = 30}}:
+g = f(Nat, 4, [1] =, 2 ,= [3])
+              ^^^^^^^^^^^^^^^
+
+  Expected vector of length 4
+from the type:  Vec(VApp VPar In checking_check_defs_1_g_1_ 0 B0, VPar In checking_check_defs_1_g_1_ 1)
+but got vector: concatEqOdd([1], 2, [3])
+of odd length
+
+