80d1a88 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix implicit spotting in case blocks

When case blocks are in types we need to check which names are bound in the case block, and not automatically bind them.

commit80d1a885b08cec21ede46841a7253601828df3c0 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 14 Jun 2014, 14:24 (12 years ago) parentb92213c

2 files changed+6−1

unifiedsplit

src/Idris/AbsSyntaxTree.hs+4−1

@@ -1663,7 +1663,10 @@ namesIn uvars ist tm = nub $ ni [] tm

16631663 _ -> if n `elem` (map fst uvars) then [n] else []

16641664 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

16651665 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1666− ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

1666+ ni env (PCase _ c os) = ni env c ++

1667+ -- names in 'os', not counting the names bound in the cases

1668+ (nub (concatMap (ni env) (map snd os))

1669+ \\ nub (concatMap (ni env) (map fst os)))

16671670 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

16681671 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

16691672 ni env (PEq _ l r) = ni env l ++ ni env r

src/Idris/ElabDecls.hs+2

@@ -969,6 +969,8 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

969969 def' <- checkDef fc defer

970970 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'

971971 addDeferred def''

972+ mapM_ (\(n, _) -> addIBC (IBCDef n)) def''

973+

972974 mapM_ (elabCaseBlock info []) is

973975 ctxt <- getContext

974976 (cty, _) <- recheckC fc [] t'