@@ -67,7 +67,7 @@ instance Show t => Show (SC' t) where
6767
6868type CaseTree = SC
6969type Clause = ([Pat], (Term, Term))
70−type CS = ([Term], Int)
70+type CS = ([Term], Int, [(Name, Type)])
7171
7272instance TermSize SC where
7373 termsize n (Case n' as) = termsize n as
@@ -204,13 +204,18 @@ simpleCase tc cover reflect phase fc cs
204204 ns = take numargs args
205205 (ns', ps') = order ns pats
206206 (tree, st) = runState
207− (match ns' ps' (defaultCase cover)) ([], numargs)
208− t = CaseDef ns (prune proj (depatt ns' tree)) (fst st) in
209− if proj then return (stripLambdas t) else return t
207+ (match ns' ps' (defaultCase cover)) ([], numargs, [])
208+ t = CaseDef ns (prune proj (depatt ns' tree)) (fstT st) in
209+ if proj then return (stripLambdas t)
210+ else if checkSameTypes (lstT st) tree
211+ then return t
212+ else Error (At fc (Msg "Typecase is not allowed"))
210213 Error err -> Error (At fc err)
211214 where args = map (\i -> MN i "e") [0..]
212215 defaultCase True = STerm Erased
213216 defaultCase False = UnmatchedCase "Error"
217+ fstT (x, _, _) = x
218+ lstT (_, _, x) = x
214219
215220 chkAccessible (avs, l, c)
216221 | phase == RunTime || reflect = return (l, c)
@@ -218,17 +223,61 @@ simpleCase tc cover reflect phase fc cs
218223 return (l, c)
219224
220225 acc [] n = Error (Inaccessible n)
221− acc (PV x : xs) n | x == n = OK ()
226+ acc (PV x t : xs) n | x == n = OK ()
222227 acc (PCon _ _ ps : xs) n = acc (ps ++ xs) n
223228 acc (PSuc p : xs) n = acc (p : xs) n
224229 acc (_ : xs) n = acc xs n
225230
231+-- For each 'Case', make sure every choice is in the same type family,
232+-- as directed by the variable type (i.e. there is no implicit type casing
233+-- going on).
234+
235+checkSameTypes :: [(Name, Type)] -> SC -> Bool
236+checkSameTypes tys (Case n alts)
237+ = case lookup n tys of
238+ Just t -> and (map (checkAlts t) alts)
239+ _ -> and (map ((checkSameTypes tys).getSC) alts)
240+ where
241+ checkAlts t (ConCase n _ _ sc) = isType n t && checkSameTypes tys sc
242+ checkAlts (Constant t) (ConstCase c sc) = isConstType c t && checkSameTypes tys sc
243+ checkAlts _ (ConstCase c sc) = False
244+ checkAlts _ _ = True
245+
246+ getSC (ConCase _ _ _ sc) = sc
247+ getSC (FnCase _ _ sc) = sc
248+ getSC (ConstCase _ sc) = sc
249+ getSC (SucCase _ sc) = sc
250+ getSC (DefaultCase sc) = sc
251+checkSameTypes _ _ = True
252+
253+-- FIXME: All we're actually doing here is checking that we haven't arrived
254+-- at a specific constructor for a polymorphic argument. I *think* this
255+-- is sufficient, but if it turns out not to be, fix it!
256+isType n t | (P (TCon _ _) _ _, _) <- unApply t = True
257+isType n t = False
258+
259+isConstType (I _) (AType (ATInt ITNative)) = True
260+isConstType (BI _) (AType (ATInt ITBig)) = True
261+isConstType (Fl _) (AType ATFloat) = True
262+isConstType (Ch _) (AType (ATInt ITChar)) = True
263+isConstType (Str _) StrType = True
264+isConstType (B8 _) (AType (ATInt _)) = True
265+isConstType (B16 _) (AType (ATInt _)) = True
266+isConstType (B32 _) (AType (ATInt _)) = True
267+isConstType (B64 _) (AType (ATInt _)) = True
268+isConstType (B8V _) (AType (ATInt _)) = True
269+isConstType (B16V _) (AType (ATInt _)) = True
270+isConstType (B32V _) (AType (ATInt _)) = True
271+isConstType (B64V _) (AType (ATInt _)) = True
272+isConstType _ _ = False
273+
226274data Pat = PCon Name Int [Pat]
227275 | PConst Const
228− | PV Name
276+ | PV Name Type
229277 | PSuc Pat -- special case for n+1 on Integer
230278 | PReflected Name [Pat]
231279 | PAny
280+ | PTyPat -- typecase, not allowed, inspect last
232281 deriving Show
233282
234283-- If there are repeated variables, take the *last* one (could be name shadowing
@@ -250,25 +299,30 @@ toPat reflect tc tms = evalState (mapM (\x -> toPat' x []) tms) []
250299 = do p' <- toPat' p []
251300 return $ PSuc p'
252301 -- Typecase
253− toPat' (P (TCon t a) n _) args | tc
254− = do args' <- mapM (\x -> toPat' x []) args
255− return $ PCon n t args'
256− toPat' (Constant (AType (ATInt ITNative))) []
257− | tc = return $ PCon (UN "Int") 1 []
258− toPat' (Constant (AType ATFloat)) [] | tc = return $ PCon (UN "Float") 2 []
259− toPat' (Constant (AType (ATInt ITChar))) [] | tc = return $ PCon (UN "Char") 3 []
260− toPat' (Constant StrType) [] | tc = return $ PCon (UN "String") 4 []
261− toPat' (Constant PtrType) [] | tc = return $ PCon (UN "Ptr") 5 []
262− toPat' (Constant (AType (ATInt ITBig))) []
263− | tc = return $ PCon (UN "Integer") 6 []
264− toPat' (Constant (AType (ATInt (ITFixed n)))) []
265− | tc = return $ PCon (UN (fixedN n)) (7 + fromEnum n) [] -- 7-10 inclusive
266− toPat' (P Bound n _) [] = do ns <- get
302+-- toPat' (P (TCon t a) n _) args | tc
303+-- = do args' <- mapM (\x -> toPat' x []) args
304+-- return $ PCon n t args'
305+-- toPat' (Constant (AType (ATInt ITNative))) []
306+-- | tc = return $ PCon (UN "Int") 1 []
307+-- toPat' (Constant (AType ATFloat)) [] | tc = return $ PCon (UN "Float") 2 []
308+-- toPat' (Constant (AType (ATInt ITChar))) [] | tc = return $ PCon (UN "Char") 3 []
309+-- toPat' (Constant StrType) [] | tc = return $ PCon (UN "String") 4 []
310+-- toPat' (Constant PtrType) [] | tc = return $ PCon (UN "Ptr") 5 []
311+-- toPat' (Constant (AType (ATInt ITBig))) []
312+-- | tc = return $ PCon (UN "Integer") 6 []
313+-- toPat' (Constant (AType (ATInt (ITFixed n)))) []
314+-- | tc = return $ PCon (UN (fixedN n)) (7 + fromEnum n) [] -- 7-10 inclusive
315+ toPat' (P Bound n ty) [] = -- trace (show (n, ty)) $
316+ do ns <- get
267317 if n `elem` ns
268318 then return PAny
269319 else do put (n : ns)
270− return (PV n)
320+ return (PV n ty)
271321 toPat' (App f a) args = toPat' f (a : args)
322+ toPat' (Constant (AType _)) [] = return PTyPat
323+ toPat' (Constant StrType) [] = return PTyPat
324+ toPat' (Constant PtrType) [] = return PTyPat
325+ toPat' (Constant VoidType) [] = return PTyPat
272326 toPat' (Constant x) [] = return $ PConst x
273327 toPat' (Bind n (Pi t) sc) [] | reflect && noOccurrence n sc
274328 = do t' <- toPat' t []
@@ -289,9 +343,10 @@ data Partition = Cons [Clause]
289343 | Vars [Clause]
290344 deriving Show
291345
292−isVarPat (PV _ : ps , _) = True
293−isVarPat (PAny : ps , _) = True
294−isVarPat _ = False
346+isVarPat (PV _ _ : ps , _) = True
347+isVarPat (PAny : ps , _) = True
348+isVarPat (PTyPat : ps , _) = True
349+isVarPat _ = False
295350
296351isConPat (PCon _ _ _ : ps, _) = True
297352isConPat (PReflected _ _ : ps, _) = True
@@ -337,8 +392,8 @@ order ns cs = let patnames = transpose (map (zip ns) (map fst cs))
337392match :: [Name] -> [Clause] -> SC -- error case
338393 -> State CS SC
339394match [] (([], ret) : xs) err
340− = do (ts, v) <- get
341− put (ts ++ (map (fst.snd) xs), v)
395+ = do (ts, v, ntys) <- get
396+ put (ts ++ (map (fst.snd) xs), v, ntys)
342397 case snd ret of
343398 Impossible -> return ImpossibleCase
344399 tm -> return $ STerm tm -- run out of arguments
@@ -408,12 +463,15 @@ argsToAlt rs@((r, m) : rest)
408463 return (newArgs, addRs rs)
409464 where
410465 getNewVars [] = return []
411− getNewVars ((PV n) : ns) = do v <- getVar "e"
412− nsv <- getNewVars ns
413− return (v : nsv)
466+ getNewVars ((PV n t) : ns) = do v <- getVar "e"
467+ nsv <- getNewVars ns
468+ return (v : nsv)
414469 getNewVars (PAny : ns) = do v <- getVar "i"
415470 nsv <- getNewVars ns
416471 return (v : nsv)
472+ getNewVars (PTyPat : ns) = do v <- getVar "t"
473+ nsv <- getNewVars ns
474+ return (v : nsv)
417475 getNewVars (_ : ns) = do v <- getVar "e"
418476 nsv <- getNewVars ns
419477 return (v : nsv)
@@ -424,7 +482,7 @@ argsToAlt rs@((r, m) : rest)
424482 uniq i n = n
425483
426484getVar :: String -> State CS Name
427−getVar b = do (t, v) <- get; put (t, v+1); return (MN v b)
485+getVar b = do (t, v, ntys) <- get; put (t, v+1, ntys); return (MN v b)
428486
429487groupCons :: [Clause] -> State CS [Group]
430488groupCons cs = gc [] cs
@@ -454,12 +512,15 @@ groupCons cs = gc [] cs
454512
455513varRule :: [Name] -> [Clause] -> SC -> State CS SC
456514varRule (v : vs) alts err =
457− do let alts' = map (repVar v) alts
515+ do alts' <- mapM (repVar v) alts
458516 match vs alts' err
459517 where
460− repVar v (PV p : ps , (lhs, res))
461− = (ps, (lhs, subst p (P Bound v Erased) res))
462− repVar v (PAny : ps , res) = (ps, res)
518+ repVar v (PV p ty : ps , (lhs, res))
519+ = do (cs, i, ntys) <- get
520+ put (cs, i, (v, ty) : ntys)
521+ return (ps, (lhs, subst p (P Bound v ty) res))
522+ repVar v (PAny : ps , res) = return (ps, res)
523+ repVar v (PTyPat : ps , res) = return (ps, res)
463524
464525-- fix: case e of S k -> f (S k) ==> case e of S k -> f e
465526