e363c09 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Better treatment of unbound implicits

Now uses the elaborator to generate any necessary extra bindings, using the same machinery as pattern match elaboration. The end result is that you no longer need 'using' in a lot of cases (it is still useful if you want to give explicit types, of course). e.g. this now works as it stands: data Elem : a -> Vect n a -> Type where Here : Elem x (x :: xs) There : Elem x xs -> Elem x (y :: xs) isElem : DecEq a => (x : a) -> (xs : _) -> Maybe (Elem x xs) This should also reduce the number of weird "no such variable" errors signfificantly. In particular, it fixes #1354

commite363c092a23bbc08c036946910656d3a58dbe09c authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 8 Jul 2014, 02:40 (12 years ago) parent3c4bd14

20 files changed+481−243

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+97−21

@@ -1078,6 +1078,16 @@ addStatics n tm ptm =

10781078

10791079-- Dealing with implicit arguments

10801080

1081+-- Add some bound implicits to the using block if they aren't there already

1082+

1083+addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]

1084+addToUsing us [] = us

1085+addToUsing us ((n, t) : ns)

1086+ | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns

1087+ | otherwise = addToUsing us ns

1088+ where impName (UImplicit n _) = Just n

1089+ impName _ = Nothing

1090+

10811091-- Add constraint bindings from using block

10821092

10831093addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm

@@ -1117,6 +1127,66 @@ addUsingConstraints syn fc t

11171127 getName (PExp _ _ _ (PRef _ n)) = return n

11181128 getName _ = []

11191129

1130+-- Add implicit bindings from using block, and bind any missing names

1131+addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm

1132+addUsingImpls syn n fc t

1133+ = do ist <- getIState

1134+ let ns = implicitNamesIn (map iname uimpls) ist t

1135+ let badnames = filter (\n -> not (implicitable n) &&

1136+ n `notElem` (map iname uimpls)) ns

1137+ when (not (null badnames)) $

1138+ throwError (At fc (Elaborating "type of " n

1139+ (NoSuchVariable (head badnames))))

1140+ let cs = getArgnames t -- get already bound names

1141+ let addimpls = filter (\n -> iname n `notElem` cs) uimpls

1142+ -- if all names in the arguments of addconsts appear in ns,

1143+ -- add the constraint implicitly

1144+ return (bindFree ns (doAdd addimpls ns t))

1145+ where uimpls = filter uimpl (using syn)

1146+ uimpl (UImplicit _ _) = True

1147+ uimpl _ = False

1148+

1149+ iname (UImplicit n _) = n

1150+ iname (UConstraint _ _) = error "Can't happen addUsingImpls"

1151+

1152+ doAdd [] _ t = t

1153+ -- if all of args in ns, then add it

1154+ doAdd (UImplicit n ty : cs) ns t

1155+ | elem n ns

1156+ = PPi (Imp [] Dynamic False) n ty (doAdd cs ns t)

1157+ | otherwise = doAdd cs ns t

1158+

1159+ -- bind the free names which weren't in the using block

1160+ bindFree [] tm = tm

1161+ bindFree (n:ns) tm

1162+ | elem n (map iname uimpls) = bindFree ns tm

1163+ | otherwise

1164+ = PPi (Imp [] Dynamic False) n Placeholder (bindFree ns tm)

1165+

1166+ getArgnames (PPi _ n c sc)

1167+ = n : getArgnames sc

1168+ getArgnames _ = []

1169+

1170+-- Given the original type and the elaborated type, return the implicitness

1171+-- status of each pi-bound argument, and whether it's inaccessible (True) or not.

1172+

1173+getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]

1174+getUnboundImplicits i (Bind n (Pi t) sc) (PPi p n' t' sc')

1175+ | n == n' = argInfo n p : getUnboundImplicits i sc sc'

1176+ where

1177+ argInfo n (Imp opt _ _) = (True, PImp (getPriority i t') True opt n t')

1178+ argInfo n (Exp opt _ _) = (InaccessibleArg `elem` opt,

1179+ PExp (getPriority i t') opt n t')

1180+ argInfo n (Constraint opt _) = (InaccessibleArg `elem` opt,

1181+ PConstraint 10 opt n t')

1182+ argInfo n (TacImp opt _ scr) = (InaccessibleArg `elem` opt,

1183+ PTacImplicit 10 opt n scr t')

1184+getUnboundImplicits i (Bind n (Pi t) sc) tm

1185+ = impBind n t : getUnboundImplicits i sc tm

1186+ where

1187+ impBind n t = (True, PImp 1 True [] n Placeholder)

1188+getUnboundImplicits i sc tm = []

1189+

11201190-- Add implicit Pi bindings for any names in the term which appear in an

11211191-- argument position.

11221192

@@ -1428,40 +1498,46 @@ aiFn inpat expat qq ist fc f ds as

14281498 _ -> Public

14291499

14301500 insertImpl :: [PArg] -> [PArg] -> [PArg]

1431− insertImpl ps as = insImpAcc M.empty ps as

1501+ insertImpl ps as = insImpAcc M.empty ps (filter exp as) (filter (not.exp) as)

1502+

1503+ exp (PExp _ _ _ _) = True

1504+ exp (PConstraint _ _ _ _) = True

1505+ exp _ = False

14321506

14331507 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms

14341508 -> [PArg] -- parameters

1435− -> [PArg] -- arguments

1509+ -> [PArg] -- explicit arguments

1510+ -> [PArg] -- implicits given

14361511 -> [PArg]

1437− insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) =

1438− PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given

1439− insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) =

1440− PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given

1441− insImpAcc pnas (PConstraint p l n ty : ps) given =

1512+ insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =

1513+ PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps

1514+ insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =

1515+ PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps

1516+ insImpAcc pnas (PConstraint p l n ty : ps) given imps =

14421517 let rtc = PResolveTC fc in

1443− PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given

1444− insImpAcc pnas (PImp p _ l n ty : ps) given =

1445− case find n given [] of

1446− Just (tm, given') ->

1447− PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given'

1518+ PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps

1519+ insImpAcc pnas (PImp p _ l n ty : ps) given imps =

1520+ case find n imps [] of

1521+ Just (tm, imps') ->

1522+ PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'

14481523 Nothing ->

14491524 PImp p True l n Placeholder :

1450− insImpAcc (M.insert n Placeholder pnas) ps given

1451− insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given =

1525+ insImpAcc (M.insert n Placeholder pnas) ps given imps

1526+ insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =

14521527 let sc = addImpl ist (substMatches (M.toList pnas) sc') in

1453− case find n given [] of

1454− Just (tm, given') ->

1528+ case find n imps [] of

1529+ Just (tm, imps') ->

14551530 PTacImplicit p l n sc tm :

1456− insImpAcc (M.insert n tm pnas) ps given'

1531+ insImpAcc (M.insert n tm pnas) ps given imps'

14571532 Nothing ->

14581533 if inpat

14591534 then PTacImplicit p l n sc Placeholder :

1460− insImpAcc (M.insert n Placeholder pnas) ps given

1535+ insImpAcc (M.insert n Placeholder pnas) ps given imps

14611536 else PTacImplicit p l n sc sc :

1462− insImpAcc (M.insert n sc pnas) ps given

1463− insImpAcc _ expected [] = []

1464− insImpAcc _ _ given = given

1537+ insImpAcc (M.insert n sc pnas) ps given imps

1538+ insImpAcc _ expected [] imps = imps -- so that unused implicits give error

1539+ -- TODO: report here, and prune alternatives

1540+ insImpAcc _ _ given imps = given ++ imps

14651541

14661542 find n [] acc = Nothing

14671543 find n (PImp _ _ _ n' t : gs) acc

src/Idris/AbsSyntaxTree.hs+36

@@ -1669,6 +1669,42 @@ boundNamesIn tm = nub $ ni tm

16691669 niTacImp (TacImp _ _ scr) = ni scr

16701670 niTacImp _ = []

16711671

1672+-- Return names which are valid implicits in the given term (type).

1673+implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]

1674+implicitNamesIn uvars ist tm = nub $ ni [] tm

1675+ where

1676+ ni env (PRef _ n)

1677+ | not (n `elem` env)

1678+ = case lookupTy n (tt_ctxt ist) of

1679+ [] -> [n]

1680+ _ -> if n `elem` uvars then [n] else []

1681+ ni env (PApp _ f@(PRef _ n) as)

1682+ | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)

1683+ | otherwise = concatMap (ni env) (map getTm as)

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

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

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

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

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

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

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

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

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

1693+ ni env (PRewrite _ l r _) = ni env l ++ ni env r

1694+ ni env (PTyped l r) = ni env l ++ ni env r

1695+ ni env (PPair _ _ l r) = ni env l ++ ni env r

1696+ ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

1697+ ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r

1698+ ni env (PAlternative a as) = concatMap (ni env) as

1699+ ni env (PHidden tm) = ni env tm

1700+ ni env (PUnifyLog tm) = ni env tm

1701+ ni env (PDisamb _ tm) = ni env tm

1702+ ni env (PNoImplicits tm) = ni env tm

1703+ ni env _ = []

1704+

1705+ niTacImp env (TacImp _ _ scr) = ni env scr

1706+ niTacImp _ _ = []

1707+

16721708-- Return names which are free in the given term.

16731709namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]

16741710namesIn uvars ist tm = nub $ ni [] tm

src/Idris/CaseSplit.hs+2−2

@@ -55,7 +55,7 @@ split n t'

5555 = do ist <- getIState

5656 -- Make sure all the names in the term are accessible

5757 mapM_ (\n -> setAccessibility n Public) (allNamesIn t')

58− (tm, ty, pats) <- elabValBind toplevel True True (addImplPat ist t')

58+ (tm, ty, pats) <- elabValBind toplevel ELHS True (addImplPat ist t')

5959 -- ASSUMPTION: tm is in normal form after elabValBind, so we don't

6060 -- need to do anything special to find out what family each argument

6161 -- is in

@@ -201,7 +201,7 @@ tidy ist tm ty = return tm

201201-- tidyVar t = t

202202

203203elabNewPat :: PTerm -> Idris (Maybe PTerm)

204−elabNewPat t = idrisCatch (do (tm, ty) <- elabVal toplevel True t

204+elabNewPat t = idrisCatch (do (tm, ty) <- elabVal toplevel ELHS t

205205 i <- getIState

206206 return (Just (delab i tm)))

207207 (\e -> do i <- getIState

src/Idris/Core/Elaborate.hs+2−1

@@ -77,6 +77,7 @@ getNameFrom n = do (ES (p, a) s e) <- get

7777 then MN (next+500) x

7878 else MN (next+100) x

7979 NS (UN x) s -> MN (next+100) x

80+ _ -> n

8081 return $! n'

8182

8283setNextName :: Elab' aux ()

@@ -456,7 +457,7 @@ prepare_apply fn imps =

456457 -> [(Name, Name)] -- ^ Accumulator for produced claims

457458 -> [Name] -- ^ Hypotheses

458459 -> Elab' aux [(Name, Name)] -- ^ The names of the arguments and their holes, resp.

459− mkClaims (Bind n' (Pi t_in) sc) (i : is) claims hs =

460+ mkClaims (Bind n' (Pi t_in) sc) (i : is) claims hs =

460461 do let t = rebind hs t_in

461462 n <- getNameFrom (mkMN n')

462463-- when (null claims) (start_unify n)

src/Idris/Core/Evaluate.hs+6

@@ -549,6 +549,12 @@ convEq ctxt holes topx topy = ceq [] topx topy where

549549 | n == n' = ceq ps x y

550550 ceq ps (Bind n (Lam t) (App x (P Bound n' _))) y

551551 | n == n' = ceq ps x y

552+

553+ ceq ps (Bind n (PVar t) sc) y = ceq ps sc y

554+ ceq ps x (Bind n (PVar t) sc) = ceq ps x sc

555+ ceq ps (Bind n (PVTy t) sc) y = ceq ps sc y

556+ ceq ps x (Bind n (PVTy t) sc) = ceq ps x sc

557+

552558 ceq ps (V x) (V y) = return (x == y)

553559 ceq ps (V x) (P _ y _)

554560 | x >= 0 && length ps > x = return (fst (ps!!x) == y)

src/Idris/Core/ProofState.hs+39−26

@@ -168,12 +168,16 @@ match_unify' ctxt env topx topy =

168168 ++ "\n" ++ show (pterm ps) ++ "\n\n"

169169 ) $

170170 case match_unify ctxt env topx topy inj (holes ps) while of

171− OK u -> do let (h, ns) = unified ps

172− put (ps { unified = (h, u ++ ns) })

173− return u

174− Error e -> do put (ps { problems = (topx, topy, env, e, while, Match) :

175− problems ps })

176− return []

171+ OK u -> traceWhen (unifylog ps)

172+ ("Matched " ++ show u) $

173+ do let (h, ns) = unified ps

174+ put (ps { unified = (h, u ++ ns) })

175+ return u

176+ Error e -> traceWhen (unifylog ps)

177+ ("No match " ++ show e) $

178+ do put (ps { problems = (topx, topy, env, e, while, Match) :

179+ problems ps })

180+ return []

177181-- traceWhen (unifylog ps)

178182-- ("Matched " ++ show (topx, topy) ++ " without " ++ show dont ++

179183-- "\nSolved: " ++ show u

@@ -231,7 +235,8 @@ unify' ctxt env topx topy =

231235 (holes ps)

232236 let (notu', probs_notu) = mergeNotunified env (notu ++ notunified ps)

233237 traceWhen (unifylog ps)

234− ("Now solved: " ++ show ns') $

238+ ("Now solved: " ++ show ns' ++

239+ "\nNow problems: " ++ qshow (probs' ++ probs_notu)) $

235240 put (ps { problems = probs' ++ probs_notu,

236241 unified = (h, ns'),

237242 injective = updateInj u (injective ps),

@@ -538,10 +543,11 @@ solve ctxt env (Bind x (Guess ty val) sc)

538543 = do ps <- get

539544 let (uh, uns) = unified ps

540545 case lookup x (notunified ps) of

541− Just tm -> -- trace ("NEED MATCH: " ++ show (tm, val)) $

546+ Just tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $

542547 match_unify' ctxt env tm val

543548 _ -> return []

544− action (\ps -> ps { holes = holes ps \\ [x],

549+ action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping hole " ++ show x) $

550+ holes ps \\ [x],

545551 solved = Just (x, val),

546552 notunified = updateNotunified [(x,val)]

547553 (notunified ps),

@@ -605,7 +611,9 @@ forall n ty ctxt env _ = fail "Can't pi bind here"

605611

606612patvar :: Name -> RunTactic

607613patvar n ctxt env (Bind x (Hole t) sc) =

608− do action (\ps -> ps { holes = holes ps \\ [x],

614+ do action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping pattern hole " ++ show x) $

615+ holes ps \\ [x],

616+ solved = Just (x, P Bound n t),

609617 notunified = updateNotunified [(x,P Bound n t)]

610618 (notunified ps),

611619 injective = addInj n x (injective ps) })

@@ -787,7 +795,8 @@ solve_unified ctxt env tm =

787795 do ps <- get

788796 let (_, ns) = unified ps

789797 let unify = dropGiven (dontunify ps) ns (holes ps)

790− action (\ps -> ps { holes = holes ps \\ map fst unify })

798+ action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping holes " ++ show (map fst unify)) $

799+ holes ps \\ map fst unify })

791800 action (\ps -> ps { pterm = updateSolved unify (pterm ps) })

792801 return (updateSolved unify tm)

793802

@@ -913,11 +922,12 @@ processTactic EndUnify ps

913922 (ns'', probs') = updateProblems (context ps) ns' (problems ps)

914923 (injective ps) (holes ps)

915924 tm' = updateSolved ns'' (pterm ps) in

916− return (ps { pterm = tm',

917− unified = (h, []),

918− problems = probs',

919− notunified = updateNotunified ns'' (notunified ps),

920− holes = holes ps \\ map fst ns'' }, "")

925+ traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns'')) $

926+ return (ps { pterm = tm',

927+ unified = (h, []),

928+ problems = probs',

929+ notunified = updateNotunified ns'' (notunified ps),

930+ holes = holes ps \\ map fst ns'' }, "")

921931processTactic UnifyAll ps

922932 = let tm' = updateSolved (notunified ps) (pterm ps) in

923933 return (ps { pterm = tm',

@@ -934,10 +944,11 @@ processTactic UnifyProblems ps

934944 (injective ps)

935945 (holes ps)

936946 pterm' = updateSolved ns' (pterm ps) in

937− return (ps { pterm = pterm', solved = Nothing, problems = probs',

938− previous = Just ps, plog = "",

939− notunified = updateNotunified ns' (notunified ps),

940− holes = holes ps \\ (map fst ns') }, plog ps)

947+ traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns')) $

948+ return (ps { pterm = pterm', solved = Nothing, problems = probs',

949+ previous = Just ps, plog = "",

950+ notunified = updateNotunified ns' (notunified ps),

951+ holes = holes ps \\ (map fst ns') }, plog ps)

941952processTactic (MatchProblems all) ps

942953 = let (ns', probs') = matchProblems all [] (context ps)

943954 (problems ps)

@@ -948,6 +959,7 @@ processTactic (MatchProblems all) ps

948959 (injective ps)

949960 (holes ps)

950961 pterm' = updateSolved ns'' (pterm ps) in

962+ traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns'')) $

951963 return (ps { pterm = pterm', solved = Nothing, problems = probs'',

952964 previous = Just ps, plog = "",

953965 notunified = updateNotunified ns'' (notunified ps),

@@ -968,12 +980,13 @@ processTactic t ps

968980 -- rechecking problems may find more solutions, so

969981 -- apply them here

970982 let pterm'' = updateSolved ns' (pterm ps')

971− return (ps' { pterm = pterm'',

972− solved = Nothing,

973− problems = probs',

974− notunified = updateNotunified ns' (notunified ps'),

975− previous = Just ps, plog = "",

976− holes = holes ps' \\ (map fst ns')}, plog ps')

983+ traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns')) $

984+ return (ps' { pterm = pterm'',

985+ solved = Nothing,

986+ problems = probs',

987+ notunified = updateNotunified ns' (notunified ps'),

988+ previous = Just ps, plog = "",

989+ holes = holes ps' \\ (map fst ns')}, plog ps')

977990

978991process :: Tactic -> Name -> StateT TState TC ()

979992process EndUnify _

src/Idris/Core/TT.hs+42−1

@@ -384,7 +384,7 @@ tcname _ = False

384384implicitable (NS n _) = implicitable n

385385implicitable (UN xs) | T.null xs = False

386386 | otherwise = isLower (T.head xs)

387−implicitable (MN _ _) = True

387+implicitable (MN _ x) = not (tnull x) && thead x /= '_'

388388implicitable _ = False

389389

390390nsroot (NS n _) = n

@@ -1264,8 +1264,11 @@ weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))

12641264orderPats :: Term -> Term

12651265orderPats tm = op [] tm

12661266 where

1267+ op [] (App f a) = App f (op [] a) -- for Infer terms

1268+

12671269 op ps (Bind n (PVar t) sc) = op ((n, PVar t) : ps) sc

12681270 op ps (Bind n (Hole t) sc) = op ((n, Hole t) : ps) sc

1271+ op ps (Bind n (Pi t) sc) = op ((n, Pi t) : ps) sc

12691272 op ps sc = bindAll (sortP ps) sc

12701273

12711274 sortP ps = pick [] (reverse ps)

@@ -1288,6 +1291,44 @@ orderPats tm = op [] tm

12881291 = (n', t') : insert n t ps

12891292 | otherwise = (n,t):(n',t'):ps

12901293

1294+-- Make sure all the pattern bindings are as far out as possible

1295+liftPats :: Term -> Term

1296+liftPats tm = let (tm', ps) = runState (getPats tm) [] in

1297+ orderPats $ bindPats (reverse ps) tm'

1298+ where

1299+ bindPats [] tm = tm

1300+ bindPats ((n, t):ps) tm

1301+ | n `notElem` map fst ps = Bind n (PVar t) (bindPats ps tm)

1302+ | otherwise = bindPats ps tm

1303+

1304+ getPats :: Term -> State [(Name, Type)] Term

1305+ getPats (Bind n (PVar t) sc) = do ps <- get

1306+ put ((n, t) : ps)

1307+ getPats sc

1308+ getPats (Bind n (Guess t v) sc) = do t' <- getPats t

1309+ v' <- getPats v

1310+ sc' <- getPats sc

1311+ return (Bind n (Guess t' v') sc')

1312+ getPats (Bind n (Let t v) sc) = do t' <- getPats t

1313+ v' <- getPats v

1314+ sc' <- getPats sc

1315+ return (Bind n (Let t' v') sc')

1316+ getPats (Bind n (Pi t) sc) = do t' <- getPats t

1317+ sc' <- getPats sc

1318+ return (Bind n (Pi t') sc')

1319+ getPats (Bind n (Lam t) sc) = do t' <- getPats t

1320+ sc' <- getPats sc

1321+ return (Bind n (Lam t') sc')

1322+ getPats (Bind n (Hole t) sc) = do t' <- getPats t

1323+ sc' <- getPats sc

1324+ return (Bind n (Hole t') sc')

1325+

1326+

1327+ getPats (App f a) = do f' <- getPats f

1328+ a' <- getPats a

1329+ return (App f' a')

1330+ getPats t = return t

1331+

12911332allTTNames :: Eq n => TT n -> [n]

12921333allTTNames = nub . allNamesIn

12931334 where allNamesIn (P _ n _) = [n]

src/Idris/Core/Unify.hs+7−5

@@ -84,11 +84,11 @@ match_unify ctxt env topx topy inj holes from =

8484 = let n' = uniqueName fn (map fst env) in

8585 checkCycle names (f, Bind n' (Lam t) x)

8686

87− un names (P _ x _) tm

88− | holeIn env x || x `elem` holes

87+ un names tx@(P _ x _) tm

88+ | tx /= tm && holeIn env x || x `elem` holes

8989 = do sc 1; checkCycle names (x, tm)

90− un names tm (P _ y _)

91− | holeIn env y || y `elem` holes

90+ un names tm ty@(P _ y _)

91+ | ty /= tm && holeIn env y || y `elem` holes

9292 = do sc 1; checkCycle names (y, tm)

9393 un bnames (V i) (P _ x _)

9494 | length bnames > i,

@@ -153,11 +153,13 @@ match_unify ctxt env topx topy inj holes from =

153153 = case lookup n as of

154154 Nothing -> combine bnames (as ++ [(n,t)]) bs

155155 Just t' -> do ns <- un bnames t t'

156− -- make sure there's n mapping from n in ns

157156 let ns' = filter (\ (x, _) -> x/=n) ns

158157 sc 1

159158 combine bnames as (ns' ++ bs)

160159

160+-- substN n tm (var, sol) = (var, subst n tm sol)

161+

162+ checkCycle ns p@(x, P _ x' _) | x == x' = return []

161163 checkCycle ns p@(x, P _ _ _) = return [p]

162164 checkCycle ns (x, tm)

163165 | not (x `elem` freeNames tm) = checkScope ns (x, tm)

src/Idris/ElabDecls.hs+140−137

@@ -71,33 +71,28 @@ checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

7171-- mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t

7272-- return (n, (i, top, t'))) ns

7373

74−-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

75−elabType :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->

76− FC -> FnOpts -> Name -> PTerm -> Idris Type

77−elabType = elabType' False

78−

79−elabType' :: Bool -> -- normalise it

80− ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->

81− FC -> FnOpts -> Name -> PTerm -> Idris Type

82−elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in

83− n = liftname info n_in in -}

84− do checkUndefined fc n

74+buildType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm ->

75+ Idris (Type, PTerm, [(Int, Name)])

76+buildType info syn fc opts n ty' = do

8577 ctxt <- getContext

8678 i <- getIState

8779

88− logLvl 5 $ show n ++ " pre-type " ++ showTmImpls ty'

80+ logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'

8981 ty' <- addUsingConstraints syn fc ty'

90− ty' <- implicit info syn n ty'

82+ ty' <- addUsingImpls syn n fc ty'

83+ let ty = addImpl i ty'

9184

92− let ty = addImpl i ty'

93− inacc = inaccessibleArgs 0 ty

94− logLvl 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

95− logLvl 5 $ show n ++ " type " ++ showTmImpls ty

96− logLvl 3 $ show n ++ ": inaccessible arguments: " ++ show inacc

85+ logLvl 3 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

86+ logLvl 3 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

9787

98− ((tyT, defer, is), log) <-

88+ ((tyT', defer, is), log) <-

9989 tclift $ elaborate ctxt n (TType (UVal 0)) []

100− (errAt "type of " n (erun fc (build i info False [] n ty)))

90+ (errAt "type of " n (erun fc (build i info ETyDecl [] n ty)))

91+

92+ let tyT = patToImp tyT'

93+

94+ logLvl 3 $ show ty ++ "\nElaborated: " ++ show tyT'

95+

10196 ds <- checkAddDef True False fc defer

10297 -- if the type is not complete, note that we'll need to infer

10398 -- things later (for solving metavariables)

@@ -107,19 +102,52 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

107102 ctxt <- getContext

108103 logLvl 5 $ "Rechecking"

109104 logLvl 6 $ show tyT

105+ logLvl 10 $ "Elaborated to " ++ showEnvDbg [] tyT

110106 (cty, _) <- recheckC fc [] tyT

111− addStatics n cty ty'

112− logLvl 6 $ "Elaborated to " ++ showEnvDbg [] tyT

107+

108+ -- record the implicit and inaccessible arguments

109+ i <- getIState

110+ let (inaccData, impls) = unzip $ getUnboundImplicits i cty ty

111+ let inacc = inaccessibleImps 0 cty inaccData

112+ logLvl 3 $ show n ++ ": inaccessible arguments: " ++ show inacc

113+

114+ putIState $ i { idris_implicits = addDef n impls (idris_implicits i) }

115+ logLvl 3 ("Implicit " ++ show n ++ " " ++ show impls)

116+ addIBC (IBCImp n)

117+

118+ return (cty, ty, inacc)

119+ where

120+ patToImp (Bind n (PVar t) sc) = Bind n (Pi t) (patToImp sc)

121+ patToImp (Bind n b sc) = Bind n b (patToImp sc)

122+ patToImp t = t

123+

124+

125+-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

126+elabType :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->

127+ FC -> FnOpts -> Name -> PTerm -> Idris Type

128+elabType = elabType' False

129+

130+elabType' :: Bool -> -- normalise it

131+ ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->

132+ FC -> FnOpts -> Name -> PTerm -> Idris Type

133+elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in

134+ n = liftname info n_in in -}

135+ do checkUndefined fc n

136+ (cty, ty, inacc) <- buildType info syn fc opts n ty'

137+

138+ addStatics n cty ty

113139 logLvl 2 $ "Rechecked to " ++ show cty

114140 let nty = cty -- normalise ctxt [] cty

115141 -- if the return type is something coinductive, freeze the definition

142+ ctxt <- getContext

116143 let nty' = normalise ctxt [] nty

117144

118145 -- Add normalised type to internals

146+ i <- getIState

119147 rep <- useREPL

120148 when rep $ do

121− addInternalApp (fc_fname fc) (fst . fc_start $ fc) (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?

122− addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (mergeTy ty' (delab i nty')))

149+ addInternalApp (fc_fname fc) (fst . fc_start $ fc) ty' -- (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?

150+ addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) ty') -- (mergeTy ty' (delab i nty')))

123151

124152 let (t, _) = unApply (getRetTy nty')

125153 let corec = case t of

@@ -163,7 +191,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

163191 -- for making an internalapp, we only want the explicit ones, and don't

164192 -- want the parameters, so just take the arguments which correspond to the

165193 -- user declared explicit ones

166− mergeTy (PPi e n ty sc) (PPi e' _ _ sc')

194+ mergeTy (PPi e n ty sc) (PPi e' n' _ sc')

167195 | e == e' = PPi e n ty (mergeTy sc sc')

168196 | otherwise = mergeTy sc sc'

169197 mergeTy _ sc = sc

@@ -184,6 +212,14 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

184212 , ns4 == map txt ["Errors","Reflection","Language"] = True

185213 tyIsHandler _ = False

186214

215+-- Get the list of (index, name) of inaccessible arguments from an elaborated

216+-- type

217+inaccessibleImps :: Int -> Type -> [Bool] -> [(Int, Name)]

218+inaccessibleImps i (Bind n (Pi t) sc) (inacc : ins)

219+ | inacc = (i, n) : inaccessibleImps (i + 1) sc ins

220+ | otherwise = inaccessibleImps (i + 1) sc ins

221+inaccessibleImps _ _ _ = []

222+

187223-- Get the list of (index, name) of inaccessible arguments from the type.

188224inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]

189225inaccessibleArgs i (PPi (Imp _ _ _) n Placeholder t)

@@ -210,42 +246,20 @@ elabData info syn doc argDocs fc opts (PLaterdecl n t_in)

210246 = do let codata = Codata `elem` opts

211247 iLOG (show (fc, doc))

212248 checkUndefined fc n

213− ctxt <- getContext

214− i <- getIState

215− -- TODO think: something more in info?

216− t_in <- implicit info syn n t_in

217− let t = addImpl i t_in

218− ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []

219− (erun fc (build i info False [] n t))

220− def' <- checkDef fc defer

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

222− addDeferredTyCon def''

249+ (cty, t, inacc) <- buildType info syn fc [] n t_in

250+

223251 addIBC (IBCDef n)

224− mapM_ (elabCaseBlock info []) is

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

226− logLvl 2 $ "---> " ++ show cty

227252 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons

228253

229254elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

230255 = do let codata = Codata `elem` opts

231256 iLOG (show fc)

232257 undef <- isUndefined fc n

233− ctxt <- getContext

234− i <- getIState

235− t_in <- implicit info syn n t_in

236− let t = addImpl i t_in

237− ((t', defer, is), log) <-

238− tclift $ elaborate ctxt n (TType (UVal 0)) []

239− (errAt "data declaration " n (erun fc (build i info False [] n t)))

240− def' <- checkDef fc defer

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

258+ (cty, t, inacc) <- buildType info syn fc [] n t_in

242259 -- if n is defined already, make sure it is just a type declaration

243260 -- with the same type we've just elaborated

244− checkDefinedAs fc n t' (tt_ctxt i)

245− addDeferredTyCon def''

246− mapM_ (elabCaseBlock info []) is

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

248− logLvl 2 $ "---> " ++ show cty

261+ i <- getIState

262+ checkDefinedAs fc n cty (tt_ctxt i)

249263 -- temporary, to check cons

250264 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)

251265 let cnameinfo = cinfo info (map cname dcons)

@@ -262,7 +276,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

262276 (idris_datatypes i) })

263277 addIBC (IBCDef n)

264278 addIBC (IBCData n)

265− checkDocs fc argDocs t_in

279+ checkDocs fc argDocs t

266280 addDocStr n doc argDocs

267281 addIBC (IBCDoc n)

268282 let metainf = DataMI params

@@ -368,6 +382,56 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

368382 liftname = id -- Is this appropriate?

369383 }

370384

385+-- FIXME: 'forcenames' is an almighty hack! Need a better way of

386+-- erasing non-forceable things

387+-- ^^^

388+-- TODO: the above is a comment from the past;

389+-- forcenames is probably no longer needed

390+elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

391+ (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)

392+elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

393+ = do checkUndefined fc n

394+ (cty, t, inacc) <- buildType info syn fc [] n (if codata then mkLazy t_in else t_in)

395+ ctxt <- getContext

396+ let cty' = normalise ctxt [] cty

397+

398+ logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t

399+ logLvl 5 $ "Inaccessible args: " ++ show inacc

400+ logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

401+

402+ addIBC (IBCDef n)

403+ checkDocs fc argDocs t

404+ addDocStr n doc argDocs

405+ addIBC (IBCDoc n)

406+ fputState (opt_inaccessible . ist_optimisation n) inacc

407+ addIBC (IBCOpt n)

408+ return (n, cty')

409+ where

410+ tyIs (Bind n b sc) = tyIs sc

411+ tyIs t | (P _ n' _, _) <- unApply t

412+ = if n' /= tn then tclift $ tfail (At fc (Msg (show n' ++ " is not " ++ show tn)))

413+ else return ()

414+ tyIs t = tclift $ tfail (At fc (Msg (show t ++ " is not " ++ show tn)))

415+

416+ mkLazy (PPi pl n ty sc)

417+ = let ty' = if getTyName ty

418+ then PApp fc (PRef fc (sUN "Lazy'"))

419+ [pexp (PRef fc (sUN "LazyCodata")),

420+ pexp ty]

421+ else ty in

422+ PPi pl n ty' (mkLazy sc)

423+ mkLazy t = t

424+

425+ getTyName (PApp _ (PRef _ n) _) = n == nsroot tn

426+ getTyName (PRef _ n) = n == nsroot tn

427+ getTyName _ = False

428+

429+

430+ getNamePos :: Int -> PTerm -> Name -> Maybe Int

431+ getNamePos i (PPi _ n _ sc) x | n == x = Just i

432+ | otherwise = getNamePos (i + 1) sc x

433+ getNamePos _ _ _ = Nothing

434+

371435type EliminatorState = StateT (Map.Map String Int) Idris

372436

373437-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)

@@ -699,15 +763,15 @@ elabProvider info syn fc what n

699763 -- First elaborate the expected type (and check that it's a type)

700764 -- The goal type for a postulate is always Type.

701765 (ty', typ) <- case what of

702− ProvTerm ty p -> elabVal toplevel False ty

703− ProvPostulate _ -> elabVal toplevel False PType

766+ ProvTerm ty p -> elabVal toplevel ERHS ty

767+ ProvPostulate _ -> elabVal toplevel ERHS PType

704768 unless (isTType typ) $

705769 ifail ("Expected a type, got " ++ show ty' ++ " : " ++ show typ)

706770

707771 -- Elaborate the provider term to TT and check that the type matches

708772 (e, et) <- case what of

709− ProvTerm _ tm -> elabVal toplevel False tm

710− ProvPostulate tm -> elabVal toplevel False tm

773+ ProvTerm _ tm -> elabVal toplevel ERHS tm

774+ ProvPostulate tm -> elabVal toplevel ERHS tm

711775 unless (isProviderOf (normalise ctxt [] ty') et) $

712776 ifail $ "Expected provider type IO (Provider (" ++

713777 show ty' ++ "))" ++ ", got " ++ show et ++ " instead."

@@ -756,7 +820,7 @@ elabTransform info fc safe lhs_in rhs_in

756820 let lhs = addImplPat i lhs_in

757821 ((lhs', dlhs, []), _) <-

758822 tclift $ elaborate ctxt (sMN 0 "transLHS") infP []

759− (erun fc (buildTC i info True [] (sUN "transform")

823+ (erun fc (buildTC i info ELHS [] (sUN "transform")

760824 (infTerm lhs)))

761825 let lhs_tm = orderPats (getInferTerm lhs')

762826 let lhs_ty = getInferType lhs'

@@ -769,7 +833,7 @@ elabTransform info fc safe lhs_in rhs_in

769833 tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty []

770834 (do pbinds i lhs_tm

771835 setNextName

772− erun fc (build i info False [] (sUN "transform") rhs)

836+ erun fc (build i info ERHS [] (sUN "transform") rhs)

773837 erun fc $ psolve lhs_tm

774838 tt <- get_term

775839 return (runState (collectDeferred Nothing tt) []))

@@ -945,70 +1009,6 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty_in

9451009 then PPi impl n' ty (implBindUp ns is t)

9461010 else implBindUp ns is t

9471011

948−-- FIXME: 'forcenames' is an almighty hack! Need a better way of

949−-- erasing non-forceable things

950−-- ^^^

951−-- TODO: the above is a comment from the past;

952−-- forcenames is probably no longer needed

953−elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

954− (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)

955−elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

956− = do checkUndefined fc n

957− ctxt <- getContext

958− i <- getIState

959− t_in <- implicit info syn n (if codata then mkLazy t_in else t_in)

960− let t = addImpl i t_in

961− logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t

962− let inacc = inaccessibleArgs 0 t

963− logLvl 5 $ "Inaccessible args: " ++ show inacc

964− ((t', defer, is), log) <-

965− tclift $ elaborate ctxt n (TType (UVal 0)) []

966− (errAt "constructor " n (erun fc (build i info False [] n t)))

967− logLvl 2 $ "Rechecking " ++ show t'

968− def' <- checkDef fc defer

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

970− addDeferred def''

971− mapM_ (\(n, _) -> addIBC (IBCDef n)) def''

972−

973− mapM_ (elabCaseBlock info []) is

974− ctxt <- getContext

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

976− let cty' = normaliseC ctxt [] cty

977− tyIs cty'

978− logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

979− addIBC (IBCDef n)

980− checkDocs fc argDocs t_in

981− addDocStr n doc argDocs

982− addIBC (IBCDoc n)

983− fputState (opt_inaccessible . ist_optimisation n) inacc

984− addIBC (IBCOpt n)

985− return (n, cty')

986− where

987− tyIs (Bind n b sc) = tyIs sc

988− tyIs t | (P _ n' _, _) <- unApply t

989− = if n' /= tn then tclift $ tfail (At fc (Msg (show n' ++ " is not " ++ show tn)))

990− else return ()

991− tyIs t = tclift $ tfail (At fc (Msg (show t ++ " is not " ++ show tn)))

992−

993− mkLazy (PPi pl n ty sc)

994− = let ty' = if getTyName ty

995− then PApp fc (PRef fc (sUN "Lazy'"))

996− [pexp (PRef fc (sUN "LazyCodata")),

997− pexp ty]

998− else ty in

999− PPi pl n ty' (mkLazy sc)

1000− mkLazy t = t

1001−

1002− getTyName (PApp _ (PRef _ n) _) = n == nsroot tn

1003− getTyName (PRef _ n) = n == nsroot tn

1004− getTyName _ = False

1005−

1006−

1007− getNamePos :: Int -> PTerm -> Name -> Maybe Int

1008− getNamePos i (PPi _ n _ sc) x | n == x = Just i

1009− | otherwise = getNamePos (i + 1) sc x

1010− getNamePos _ _ _ = Nothing

1011−

10121012-- | Elaborate a collection of left-hand and right-hand pairs - that is, a

10131013-- top-level definition.

10141014elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

@@ -1322,7 +1322,7 @@ elabPE info fc caller r =

13221322

13231323-- Elaborate a value, returning any new bindings created (this will only

13241324-- happen if elaborating as a pattern clause)

1325−elabValBind :: ElabInfo -> Bool -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])

1325+elabValBind :: ElabInfo -> ElabMode -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])

13261326elabValBind info aspat norm tm_in

13271327 = do ctxt <- getContext

13281328 i <- getIState

@@ -1356,7 +1356,7 @@ elabValBind info aspat norm tm_in

13561356

13571357 return (vtm, vty, bargs)

13581358

1359−elabVal :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type)

1359+elabVal :: ElabInfo -> ElabMode -> PTerm -> Idris (Term, Type)

13601360elabVal info aspat tm_in

13611361 = do (tm, ty, _) <- elabValBind info aspat False tm_in

13621362 return (tm, ty)

@@ -1371,7 +1371,7 @@ checkPossible info fc tcgen fname lhs_in

13711371 let lhs = addImplPat i lhs_in

13721372 -- if the LHS type checks, it is possible

13731373 case elaborate ctxt (sMN 0 "patLHS") infP []

1374− (erun fc (buildTC i info True [] fname (infTerm lhs))) of

1374+ (erun fc (buildTC i info ELHS [] fname (infTerm lhs))) of

13751375 OK ((lhs', _, _), _) ->

13761376 do let lhs_tm = orderPats (getInferTerm lhs')

13771377 case recheck ctxt [] (forget lhs_tm) lhs_tm of

@@ -1524,7 +1524,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

15241524 (((lhs', dlhs, []), probs, inj), _) <-

15251525 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

15261526 (do res <- errAt "left hand side of " fname

1527− (erun fc (buildTC i info True opts fname (infTerm lhs)))

1527+ (erun fc (buildTC i info ELHS opts fname (infTerm lhs)))

15281528 probs <- get_probs

15291529 inj <- get_inj

15301530 return (res, probs, inj))

@@ -1582,7 +1582,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

15821582 mapM_ setinj (nub (params ++ inj))

15831583 setNextName

15841584 (_, _, is) <- errAt "right hand side of " fname

1585− (erun fc (build i winfo False opts fname rhs))

1585+ (erun fc (build i winfo ERHS opts fname rhs))

15861586 errAt "right hand side of " fname

15871587 (erun fc $ psolve lhs_tm)

15881588 hs <- get_holes

@@ -1716,7 +1716,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

17161716 ((lhs', dlhs, []), _) <-

17171717 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

17181718 (errAt "left hand side of with in " fname

1719− (erun fc (buildTC i info True opts fname (infTerm lhs))) )

1719+ (erun fc (buildTC i info ELHS opts fname (infTerm lhs))) )

17201720 let lhs_tm = orderPats (getInferTerm lhs')

17211721 let lhs_ty = getInferType lhs'

17221722 let ret_ty = getRetTy lhs_ty

@@ -1734,7 +1734,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

17341734 setNextName

17351735 -- TODO: may want where here - see winfo abpve

17361736 (_', d, is) <- errAt "with value in " fname

1737− (erun fc (build i info False opts fname (infTerm wval)))

1737+ (erun fc (build i info ERHS opts fname (infTerm wval)))

17381738 erun fc $ psolve lhs_tm

17391739 tt <- get_term

17401740 return (tt, d, is))

@@ -1797,7 +1797,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

17971797 tclift $ elaborate ctxt (sMN 0 "wpatRHS") clhsty []

17981798 (do pbinds i lhs_tm

17991799 setNextName

1800− (_, d, is) <- erun fc (build i info False opts fname rhs)

1800+ (_, d, is) <- erun fc (build i info ERHS opts fname rhs)

18011801 psolve lhs_tm

18021802 tt <- get_term

18031803 return (tt, d, is))

@@ -1874,11 +1874,14 @@ data MArgTy = IA | EA | CA deriving Show

18741874elabClass :: ElabInfo -> SyntaxInfo -> Docstring ->

18751875 FC -> [PTerm] ->

18761876 Name -> [(Name, PTerm)] -> [(Name, Docstring)] -> [PDecl] -> Idris ()

1877−elabClass info syn doc fc constraints tn ps pDocs ds

1877+elabClass info syn_in doc fc constraints tn ps pDocs ds

18781878 = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

18791879 let tty = pibind ps PType

18801880 let constraint = PApp fc (PRef fc tn)

18811881 (map (pexp . PRef fc) (map fst ps))

1882+

1883+ let syn = syn_in { using = addToUsing (using syn_in) ps }

1884+

18821885 -- build data declaration

18831886 let mdecls = filter tydecl ds -- method declarations

18841887 let idecls = filter instdecl ds -- default superclass instance declarations

@@ -1904,12 +1907,12 @@ elabClass info syn doc fc constraints tn ps pDocs ds

19041907 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc pDocs fc [] ddecl

19051908 -- for each constraint, build a top level function to chase it

19061909 logLvl 5 $ "Building functions"

1907− let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps

1908− ++ using syn }

1909− fns <- mapM (cfun cn constraint usyn (map fst imethods)) constraints

1910+-- let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps

1911+-- ++ using syn }

1912+ fns <- mapM (cfun cn constraint syn (map fst imethods)) constraints

19101913 mapM_ (elabDecl EAll info) (concat fns)

19111914 -- for each method, build a top level function

1912− fns <- mapM (tfun cn constraint usyn (map fst imethods)) imethods

1915+ fns <- mapM (tfun cn constraint syn (map fst imethods)) imethods

19131916 mapM_ (elabDecl EAll info) (concat fns)

19141917 -- add the default definitions

19151918 mapM_ (elabDecl EAll info) (concat (map (snd.snd) defs))

@@ -2154,7 +2157,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

21542157 ctxt <- getContext

21552158 ((tyT, _, _), _) <-

21562159 tclift $ elaborate ctxt iname (TType (UVal 0)) []

2157− (errAt "type of " iname (erun fc (build i info False [] iname ty)))

2160+ (errAt "type of " iname (erun fc (build i info ERHS [] iname ty)))

21582161 ctxt <- getContext

21592162 (cty, _) <- recheckC fc [] tyT

21602163 let nty = normalise ctxt [] cty

src/Idris/ElabTerm.hs+49−26

@@ -29,6 +29,9 @@ import qualified Data.Text as T

2929

3030import Debug.Trace

3131

32+data ElabMode = ETyDecl | ELHS | ERHS

33+ deriving Eq

34+

3235-- Using the elaborator, convert a term in raw syntax to a fully

3336-- elaborated, typechecked term.

3437--

@@ -37,10 +40,10 @@ import Debug.Trace

3740

3841-- Also find deferred names in the term and their types

3942

40−build :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->

43+build :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

4144 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

42−build ist info pattern opts fn tm

43− = do elab ist info pattern opts fn tm

45+build ist info emode opts fn tm

46+ = do elab ist info emode opts fn tm

4447 let tmIn = tm

4548 let inf = case lookupCtxt fn (idris_tyinfodata ist) of

4649 [TIPartial] -> True

@@ -80,20 +83,32 @@ build ist info pattern opts fn tm

8083 ((_,_,_,e,_,_):es) -> traceWhen u ("Final problems:\n" ++ show probs) $

8184 if inf then return ()

8285 else lift (Error e)

86+

87+ when tydecl (do update_term orderPats

88+ mkPat)

89+-- update_term liftPats)

8390 is <- getAux

8491 tt <- get_term

8592 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

8693 log <- getLog

8794 if (log /= "") then trace log $ return (tm, ds, is)

8895 else return (tm, ds, is)

96+ where pattern = emode == ELHS

97+ tydecl = emode == ETyDecl

98+

99+ mkPat = do hs <- get_holes

100+ tm <- get_term

101+ case hs of

102+ (h: hs) -> do patvar h; mkPat

103+ [] -> return ()

89104

90105-- Build a term autogenerated as a typeclass method definition

91106-- (Separate, so we don't go overboard resolving things that we don't

92107-- know about yet on the LHS of a pattern def)

93108

94−buildTC :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->

109+buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

95110 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

96−buildTC ist info pattern opts fn tm

111+buildTC ist info emode opts fn tm

97112 = do -- set name supply to begin after highest index in tm

98113 let ns = allNamesIn tm

99114 let tmIn = tm

@@ -101,7 +116,7 @@ buildTC ist info pattern opts fn tm

101116 [TIPartial] -> True

102117 _ -> False

103118 initNextNameFrom ns

104− elab ist info pattern opts fn tm

119+ elab ist info emode opts fn tm

105120 probs <- get_probs

106121 tm <- get_term

107122 case probs of

@@ -114,13 +129,14 @@ buildTC ist info pattern opts fn tm

114129 log <- getLog

115130 if (log /= "") then trace log $ return (tm, ds, is)

116131 else return (tm, ds, is)

132+ where pattern = emode == ELHS

117133

118134-- Returns the set of declarations we need to add to complete the definition

119135-- (most likely case blocks to elaborate)

120136

121−elab :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->

137+elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

122138 ElabD ()

123−elab ist info pattern opts fn tm

139+elab ist info emode opts fn tm

124140 = do let loglvl = opt_logLevel (idris_options ist)

125141 when (loglvl > 5) $ unifyLog True

126142 compute -- expand type synonyms, etc

@@ -133,12 +149,15 @@ elab ist info pattern opts fn tm

133149 unifyProblems

134150 mkPat)

135151 where

152+ pattern = emode == ELHS

153+ bindfree = emode == ETyDecl || emode == ELHS

154+

136155 tcgen = Dictionary `elem` opts

137156 reflection = Reflection `elem` opts

138157

139158 isph arg = case getTm arg of

140159 Placeholder -> (True, priority arg)

141− _ -> (False, priority arg)

160+ tm -> (False, priority arg)

142161

143162 toElab ina arg = case getTm arg of

144163 Placeholder -> Nothing

@@ -290,25 +309,29 @@ elab ist info pattern opts fn tm

290309 trySeq' deferr [] = proofFail deferr

291310 trySeq' deferr (x : xs)

292311 = try' (elab' ina x) (trySeq' deferr xs) True

293− elab' ina (PPatvar fc n) | pattern = patvar n

312+ elab' ina (PPatvar fc n) | bindfree = do patvar n; -- update_term liftPats

294313-- elab' (_, _, inty) (PRef fc f)

295314-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty

296315-- = lift $ tfail (Msg "Typecase is not allowed")

297− elab' (ina, guarded, inty, qq) (PRef fc n) | pattern && not (inparamBlock n) && not qq

316+ elab' (ina, guarded, inty, qq) (PRef fc n)

317+ | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not qq

298318 = do ctxt <- get_context

299319 let defined = case lookupTy n ctxt of

300320 [] -> False

301321 _ -> True

302322 -- this is to stop us resolve type classes recursively

303323 -- trace (show (n, guarded)) $

304− if (tcname n && ina) then erun fc $ patvar n

324+ if (tcname n && ina) then erun fc $ do patvar n; -- update_term liftPats

305325 else if (defined && not guarded)

306326 then do apply (Var n) []; solve

307327 else try (do apply (Var n) []; solve)

308− (patvar n)

328+ (do patvar n; ) -- update_term liftPats)

309329 where inparamBlock n = case lookupCtxtName n (inblock info) of

310330 [] -> False

311331 _ -> True

332+ bindable (NS _ _) = False

333+ bindable (UN xs) = True

334+ bindable n = implicitable n

312335 elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])

313336 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve

314337 elab' ina@(_, a, inty, qq) (PLam n Placeholder sc)

@@ -924,11 +947,11 @@ findInstances ist t

924947 | otherwise = []

925948

926949trivial' ist

927− = trivial (elab ist toplevel False [] (sMN 0 "tac")) ist

950+ = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist

928951proofSearch' ist rec depth prv top n hints

929952 = do unifyProblems

930953 proofSearch rec prv depth

931− (elab ist toplevel False [] (sMN 0 "tac")) top n hints ist

954+ (elab ist toplevel ERHS [] (sMN 0 "tac")) top n hints ist

932955

933956resolveTC :: Int -> Term -> Name -> IState -> ElabD ()

934957resolveTC = resTC' []

@@ -1048,7 +1071,7 @@ case_ ind autoSolve ist fn tm = do

10481071 letn <- getNameFrom (sMN 0 "irule")

10491072 letbind letn (Var tyn) (Var valn)

10501073 focus valn

1051− elab ist toplevel False [] (sMN 0 "tac") tm

1074+ elab ist toplevel ERHS [] (sMN 0 "tac") tm

10521075 env <- get_env

10531076 let (Just binding) = lookup letn env

10541077 let val = binderVal binding

@@ -1081,7 +1104,7 @@ runTac autoSolve ist fn tac

10811104 where

10821105 bname (Bind n _ _) = Just n

10831106 bname _ = Nothing

1084− runT (Exact tm) = do elab ist toplevel False [] (sMN 0 "tac") tm

1107+ runT (Exact tm) = do elab ist toplevel ERHS [] (sMN 0 "tac") tm

10851108 when autoSolve solveAll

10861109 runT (MatchRefine fn)

10871110 = do fnimps <-

@@ -1130,7 +1153,7 @@ runTac autoSolve ist fn tac

11301153 letn <- getNameFrom (sMN 0 "equiv_val")

11311154 letbind letn (Var tyn) (Var valn)

11321155 focus tyn

1133− elab ist toplevel False [] (sMN 0 "tac") tm

1156+ elab ist toplevel ERHS [] (sMN 0 "tac") tm

11341157 focus valn

11351158 when autoSolve solveAll

11361159 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that

@@ -1143,7 +1166,7 @@ runTac autoSolve ist fn tac

11431166 letn <- getNameFrom (sMN 0 "rewrite_rule")

11441167 letbind letn (Var tyn) (Var valn)

11451168 focus valn

1146− elab ist toplevel False [] (sMN 0 "tac") tm

1169+ elab ist toplevel ERHS [] (sMN 0 "tac") tm

11471170 rewrite (Var letn)

11481171 when autoSolve solveAll

11491172 runT (Induction tm) -- let bind tm, similar to the others

@@ -1159,7 +1182,7 @@ runTac autoSolve ist fn tac

11591182 letn <- unique_hole n

11601183 letbind letn (Var tyn) (Var valn)

11611184 focus valn

1162− elab ist toplevel False [] (sMN 0 "tac") tm

1185+ elab ist toplevel ERHS [] (sMN 0 "tac") tm

11631186 when autoSolve solveAll

11641187 runT (LetTacTy n ty tm)

11651188 = do attack

@@ -1170,9 +1193,9 @@ runTac autoSolve ist fn tac

11701193 letn <- unique_hole n

11711194 letbind letn (Var tyn) (Var valn)

11721195 focus tyn

1173− elab ist toplevel False [] (sMN 0 "tac") ty

1196+ elab ist toplevel ERHS [] (sMN 0 "tac") ty

11741197 focus valn

1175− elab ist toplevel False [] (sMN 0 "tac") tm

1198+ elab ist toplevel ERHS [] (sMN 0 "tac") tm

11761199 when autoSolve solveAll

11771200 runT Compute = compute

11781201 runT Trivial = do trivial' ist; when autoSolve solveAll

@@ -1192,7 +1215,7 @@ runTac autoSolve ist fn tac

11921215 scriptvar <- getNameFrom (sMN 0 "scriptvar" )

11931216 letbind scriptvar scriptTy (Var script)

11941217 focus script

1195− elab ist toplevel False [] (sMN 0 "tac") tm

1218+ elab ist toplevel ERHS [] (sMN 0 "tac") tm

11961219 (script', _) <- get_type_val (Var scriptvar)

11971220 -- now that we have the script apply

11981221 -- it to the reflected goal and context

@@ -1225,7 +1248,7 @@ runTac autoSolve ist fn tac

12251248 letbind scriptvar scriptTy (Var script)

12261249 focus script

12271250 ptm <- get_term

1228− elab ist toplevel False [] (sMN 0 "tac")

1251+ elab ist toplevel ERHS [] (sMN 0 "tac")

12291252 (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])

12301253 (script', _) <- get_type_val (Var scriptvar)

12311254 -- now that we have the script apply

@@ -1253,7 +1276,7 @@ runTac autoSolve ist fn tac

12531276 letn <- getNameFrom (sMN 0 "letvar")

12541277 letbind letn (Var tyn) (Var valn)

12551278 focus valn

1256− elab ist toplevel False [] (sMN 0 "tac") v

1279+ elab ist toplevel ERHS [] (sMN 0 "tac") v

12571280 (value, _) <- get_type_val (Var letn)

12581281 ctxt <- get_context

12591282 env <- get_env

@@ -1267,7 +1290,7 @@ runTac autoSolve ist fn tac

12671290 letn <- getNameFrom (sMN 0 "letvar")

12681291 letbind letn (Var tyn) (Var valn)

12691292 focus valn

1270− elab ist toplevel False [] (sMN 0 "tac") v

1293+ elab ist toplevel ERHS [] (sMN 0 "tac") v

12711294 (value, _) <- get_type_val (Var letn)

12721295 ctxt <- get_context

12731296 env <- get_env

src/Idris/Interactive.hs+2−1

@@ -12,6 +12,7 @@ import Idris.Core.Evaluate

1212import Idris.CaseSplit

1313import Idris.AbsSyntax

1414import Idris.ElabDecls

15+import Idris.ElabTerm

1516import Idris.Error

1617import Idris.Delaborate

1718import Idris.Output

@@ -173,7 +174,7 @@ doProofSearch h fn updatefile rec l n hints (Just depth)

173174 let def = PClause fc mn (PRef fc mn) [] (body top) []

174175 newmv <- idrisCatch

175176 (do elabDecl' EAll toplevel (PClauses fc [] mn [def])

176− (tm, ty) <- elabVal toplevel False (PRef fc mn)

177+ (tm, ty) <- elabVal toplevel ERHS (PRef fc mn)

177178 ctxt <- getContext

178179 i <- getIState

179180 return . flip displayS "" . renderPretty 1.0 80 $

src/Idris/Prover.hs+2−2

@@ -264,7 +264,7 @@ ploop fn d prompt prf e h

264264 let OK env = envAtFocus (proof e)

265265 ctxt' = envCtxt env ctxt

266266 putIState ist { tt_ctxt = ctxt' }

267− (tm, ty) <- elabVal toplevel False t

267+ (tm, ty) <- elabVal toplevel ERHS t

268268 let ppo = ppOptionIst ist

269269 ty' = normaliseC ctxt [] ty

270270 h = idris_outh ist

@@ -288,7 +288,7 @@ ploop fn d prompt prf e h

288288 ist' = ist { tt_ctxt = ctxt' }

289289 bnd = map (\x -> (fst x, False)) env

290290 putIState ist'

291− (tm, ty) <- elabVal toplevel False t

291+ (tm, ty) <- elabVal toplevel ERHS t

292292 let tm' = force (normaliseAll ctxt' env tm)

293293 ty' = force (normaliseAll ctxt' env ty)

294294 ppo = ppOption (idris_options ist')

src/Idris/REPL.hs+11−11

@@ -651,7 +651,7 @@ process h fn (ChangeDirectory f)

651651 return ()

652652process h fn (Eval t)

653653 = withErrorReflection $ do logLvl 5 $ show t

654− (tm, ty) <- elabVal toplevel False t

654+ (tm, ty) <- elabVal toplevel ERHS t

655655 ctxt <- getContext

656656 let tm' = force (normaliseAll ctxt [] tm)

657657 let ty' = force (normaliseAll ctxt [] ty)

@@ -681,7 +681,7 @@ process h fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++

681681 elabClauses toplevel fc opts name (concatMap getClauses decls)

682682 defineName [PClauses fc opts _ [clause]] = do

683683 let pterm = getRHS clause

684− (tm,ty) <- elabVal toplevel False pterm

684+ (tm,ty) <- elabVal toplevel ERHS pterm

685685 ctxt <- getContext

686686 let tm' = force (normaliseAll ctxt [] tm)

687687 let ty' = force (normaliseAll ctxt [] ty)

@@ -699,7 +699,7 @@ process h fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++

699699process h fn (ExecVal t)

700700 = do ctxt <- getContext

701701 ist <- getIState

702− (tm, ty) <- elabVal toplevel False t

702+ (tm, ty) <- elabVal toplevel ERHS t

703703-- let tm' = normaliseAll ctxt [] tm

704704 let ty' = normaliseAll ctxt [] ty

705705 res <- execute tm

@@ -743,7 +743,7 @@ process h fn (Check (PRef _ n))

743743

744744

745745process h fn (Check t)

746− = do (tm, ty) <- elabVal toplevel False t

746+ = do (tm, ty) <- elabVal toplevel ERHS t

747747 ctxt <- getContext

748748 ist <- getIState

749749 let ppo = ppOptionIst ist

@@ -838,7 +838,7 @@ process h fn (MakeLemma updatefile l n)

838838process h fn (DoProofSearch updatefile rec l n hints)

839839 = doProofSearch h fn updatefile rec l n hints Nothing

840840process h fn (Spec t)

841− = do (tm, ty) <- elabVal toplevel False t

841+ = do (tm, ty) <- elabVal toplevel ERHS t

842842 ctxt <- getContext

843843 ist <- getIState

844844 let tm' = simplify ctxt [] {- (idris_statics ist) -} tm

@@ -917,13 +917,13 @@ process h fn (Prove n')

917917 warnTotality

918918

919919process h fn (HNF t)

920− = do (tm, ty) <- elabVal toplevel False t

920+ = do (tm, ty) <- elabVal toplevel ERHS t

921921 ctxt <- getContext

922922 ist <- getIState

923923 let tm' = hnf ctxt [] tm

924924 iPrintResult (show (delab ist tm'))

925925process h fn (TestInline t)

926− = do (tm, ty) <- elabVal toplevel False t

926+ = do (tm, ty) <- elabVal toplevel ERHS t

927927 ctxt <- getContext

928928 ist <- getIState

929929 let tm' = inlineTerm ist tm

@@ -932,7 +932,7 @@ process h fn (TestInline t)

932932process h fn Execute

933933 = idrisCatch

934934 (do ist <- getIState

935− (m, _) <- elabVal toplevel False

935+ (m, _) <- elabVal toplevel ERHS

936936 (PApp fc

937937 (PRef fc (sUN "run__IO"))

938938 [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

@@ -948,7 +948,7 @@ process h fn Execute

948948 (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

949949 where fc = fileFC "main"

950950process h fn (Compile codegen f)

951− = do (m, _) <- elabVal toplevel False

951+ = do (m, _) <- elabVal toplevel ERHS

952952 (PApp fc (PRef fc (sUN "run__IO"))

953953 [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

954954 compile codegen f m

@@ -956,7 +956,7 @@ process h fn (Compile codegen f)

956956process h fn (LogLvl i) = setLogLevel i

957957-- Elaborate as if LHS of a pattern (debug command)

958958process h fn (Pattelab t)

959− = do (tm, ty) <- elabVal toplevel True t

959+ = do (tm, ty) <- elabVal toplevel ELHS t

960960 iPrintResult $ show tm ++ "\n\n : " ++ show ty

961961

962962process h fn (Missing n)

@@ -1374,7 +1374,7 @@ execScript expr = do i <- getIState

13741374 Failure err -> do iputStrLn $ show (fixColour c err)

13751375 runIO $ exitWith (ExitFailure 1)

13761376 Success term -> do ctxt <- getContext

1377− (tm, _) <- elabVal toplevel False term

1377+ (tm, _) <- elabVal toplevel ERHS term

13781378 res <- execute tm

13791379 runIO $ exitWith ExitSuccess

13801380

test/basic001/basic001a.idrnew file+32

@@ -0,0 +1,32 @@

1+module Main

3+data RLE : Vect n Char -> Type where

4+ REnd : RLE []

5+ RChar : {xs : Vect k Char} ->

6+ (n : Nat) -> (c : Char) -> (rs : RLE xs) ->

7+ RLE (replicate (S n) c ++ xs)

9+------------

10+

11+rle : (xs : Vect n Char) -> RLE xs

12+rle [] = REnd

13+rle (x :: xs) with (rle xs)

14+ rle (x :: []) | REnd = RChar 0 x REnd

15+ rle (x :: (c :: (replicate n c ++ ys))) | (RChar n c rs) with (decEq x c)

16+ rle (x :: (x :: (replicate n x ++ ys))) | (RChar n x rs) | (Yes refl)

17+ = RChar (S n) x rs

18+ rle (x :: (c :: (replicate n c ++ ys))) | (RChar n c rs) | (No f)

19+ = RChar 0 x (RChar n c rs)

20+

21+compress : Vect n Char -> String

22+compress xs with (rle xs)

23+ compress [] | REnd = ""

24+ compress (c :: (replicate n c ++ xs1)) | (RChar n c rs)

25+ = show (the Integer (cast (S n))) ++

26+ strCons c (compress xs1)

27+

28+compressString : String -> String

29+compressString xs = compress (fromList (unpack xs))

30+

31+main : IO ()

32+main = putStrLn (compressString "foooobaaaarbaaaz")

test/basic001/expected+1

@@ -1 +1,2 @@

111f4o1b4a1r1b3a1z

2+1f4o1b4a1r1b3a1z

test/basic001/run+3−1

@@ -1,4 +1,6 @@

11#!/usr/bin/env bash

22idris $@ reg005.idr -o reg005

3+idris $@ basic001a.idr -o basic001a

34./reg005

4−rm -f reg005 *.ibc

5+./basic001a

6+rm -f reg005 basic001a *.ibc

test/error003/expected+1−1

@@ -1,2 +1,2 @@

11ErrorReflection.idr:67:5:When elaborating right hand side of bad:

2−DSL type error: (t(503) => t'(504)) doesn't match ()

2+DSL type error: (t(502) => t'(503)) doesn't match ()

test/proof007/expected+2−1

@@ -1 +1,2 @@

1−No such variable sadgjhsag

1+DefaultArgUnknownName.idr:3:18:When elaborating type of DefaultArgUnknownName.funWithBadDefArg:

2+Can't infer type for sadgjhsag

test/reg003/expected+1−1

@@ -1,2 +1,2 @@

1−reg003a.idr:4:20:When elaborating constructor Main.ECons:

1+reg003a.idr:4:11:When elaborating type of Main.ECons:

22No such variable OddList

test/reg034/expected+6−6

@@ -1,24 +1,24 @@

11reg034.idr:6:5:When elaborating left hand side of bar:

22When elaborating an application of main.bar:

33 Can't unify

4− [92mlength[0m [95mys[0m [94m=[0m [92mlength[0m [95mys[0m

4+ [92mlength[0m ys [94m=[0m [92mlength[0m ys

55 with

6− [92mlength[0m [95mxs[0m [94m=[0m [92mlength[0m [95mys[0m

6+ [92mlength[0m [95mxs[0m [94m=[0m [92mlength[0m ys

88 Specifically:

99 Can't unify

10− [92mlength[0m [95mys[0m

10+ [92mlength[0m ys

1111 with

1212 [92mlength[0m [95mxs[0m

1313reg034.idr:9:5:When elaborating left hand side of foo:

1414When elaborating an application of main.foo:

1515 Can't unify

16− [95mf[0m [95my[0m [94m=[0m [95mf[0m [95my[0m

16+ [95mf[0m y [94m=[0m [95mf[0m y

1717 with

18− [95mf[0m [95mx[0m [94m=[0m [95mf[0m [95my[0m

18+ [95mf[0m [95mx[0m [94m=[0m [95mf[0m y

1919

2020 Specifically:

2121 Can't unify

22− [95mf[0m [95my[0m

22+ [95mf[0m y

2323 with

2424 [95mf[0m [95mx[0m