f7ea42c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1726 from jfdm/fix/lift-fixme-todo

f7ea42cEdwin Brady12 years ago

src/Idris/Core/CaseTree.hs+28−24

compare with master

unifiedsplit

@@ -41,7 +41,7 @@ deriving instance Binary SC'

41deriving instance NFData SC'

42!-}

44−data CaseType = Updatable | Shared

44+data CaseType = Updatable | Shared

45 deriving (Eq, Ord, Show)

47type SC = SC' Term

@@ -184,7 +184,7 @@ directUse fn@(App f a)

184 fce == txt "Force"

185 = directUse a -- forcing a value counts as a use

186 | (P Ref n _, args) <- unApply fn = [] -- need to know what n does with them

187− | (P (TCon _ _) n _, args) <- unApply fn = [] -- type constructors not used at runtime

187+ | (P (TCon _ _) n _, args) <- unApply fn = [] -- type constructors not used at runtime

188 | otherwise = nub $ directUse f ++ directUse a

189directUse (Proj x i) = nub $ directUse x

190directUse _ = []

@@ -258,13 +258,15 @@ simpleCase tc cover reflect phase fc inacc argtys cs erInfo

258 ns = take numargs args

259 (ns', ps') = order [(n, i `elem` inacc) | (i,n) <- zip [0..] ns] pats

260 (tree, st) = runCaseBuilder erInfo

261− (match ns' ps' (defaultCase cover))

261+ (match ns' ps' (defaultCase cover))

262 ([], numargs, [])

263 t = CaseDef ns (prune proj (depatt ns' tree)) (fstT st) in

264− if proj then return (stripLambdas t)

264+ if proj then return (stripLambdas t)

265 else return t

266-- FIXME: This check is not quite right in some cases, and is breaking

267-- perfectly valid code!

268+--

269+-- Issue #1717 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1717

268-- if checkSameTypes (lstT st) tree

270-- if checkSameTypes (lstT st) tree

269-- then return t

271-- then return t

270-- else Error (At fc (Msg "Typecase is not allowed"))

272-- else Error (At fc (Msg "Typecase is not allowed"))

@@ -311,23 +313,25 @@ checkSameTypes _ _ = True

311-- FIXME: All we're actually doing here is checking that we haven't arrived

313-- FIXME: All we're actually doing here is checking that we haven't arrived

312-- at a specific constructor for a polymorphic argument. I *think* this

314-- at a specific constructor for a polymorphic argument. I *think* this

313-- is sufficient, but if it turns out not to be, fix it!

315-- is sufficient, but if it turns out not to be, fix it!

316+--

317+-- Issue #1718 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1718

314isType n t | (P (TCon _ _) _ _, _) <- unApply t = True

318isType n t | (P (TCon _ _) _ _, _) <- unApply t = True

315isType n t | (P Ref _ _, _) <- unApply t = True

319isType n t | (P Ref _ _, _) <- unApply t = True

316isType n t = False

320isType n t = False

317

321

318−isConstType (I _) (AType (ATInt ITNative)) = True

322+isConstType (I _) (AType (ATInt ITNative)) = True

319−isConstType (BI _) (AType (ATInt ITBig)) = True

323+isConstType (BI _) (AType (ATInt ITBig)) = True

320−isConstType (Fl _) (AType ATFloat) = True

324+isConstType (Fl _) (AType ATFloat) = True

321−isConstType (Ch _) (AType (ATInt ITChar)) = True

325+isConstType (Ch _) (AType (ATInt ITChar)) = True

322−isConstType (Str _) StrType = True

326+isConstType (Str _) StrType = True

323−isConstType (B8 _) (AType (ATInt _)) = True

327+isConstType (B8 _) (AType (ATInt _)) = True

324−isConstType (B16 _) (AType (ATInt _)) = True

328+isConstType (B16 _) (AType (ATInt _)) = True

325−isConstType (B32 _) (AType (ATInt _)) = True

329+isConstType (B32 _) (AType (ATInt _)) = True

326−isConstType (B64 _) (AType (ATInt _)) = True

330+isConstType (B64 _) (AType (ATInt _)) = True

327−isConstType (B8V _) (AType (ATInt _)) = True

331+isConstType (B8V _) (AType (ATInt _)) = True

328−isConstType (B16V _) (AType (ATInt _)) = True

332+isConstType (B16V _) (AType (ATInt _)) = True

329−isConstType (B32V _) (AType (ATInt _)) = True

333+isConstType (B32V _) (AType (ATInt _)) = True

330−isConstType (B64V _) (AType (ATInt _)) = True

334+isConstType (B64V _) (AType (ATInt _)) = True

331isConstType _ _ = False

335isConstType _ _ = False

332

336

333data Pat = PCon Bool Name Int [Pat]

337data Pat = PCon Bool Name Int [Pat]

@@ -430,10 +434,10 @@ order ns' cs = let patnames = transpose (map (zip ns') (map fst cs))

430 -- constructor tags between families, and no constructor/constant

434 -- constructor tags between families, and no constructor/constant

431 -- clash, because otherwise we can't reliable make the

435 -- clash, because otherwise we can't reliable make the

432 -- case distinction on evaluation

436 -- case distinction on evaluation

433− (patnames_ord, patnames_rest)

437+ (patnames_ord, patnames_rest)

434 = Data.List.partition (noClash . map snd) patnames

438 = Data.List.partition (noClash . map snd) patnames

435 -- note: sortBy . reverse is not nonsense because sortBy is stable

439 -- note: sortBy . reverse is not nonsense because sortBy is stable

436− pats' = transpose (sortBy moreDistinct (reverse patnames_ord)

440+ pats' = transpose (sortBy moreDistinct (reverse patnames_ord)

437 ++ patnames_rest) in

441 ++ patnames_rest) in

438 (getNOrder pats', zipWith rebuild pats' cs)

442 (getNOrder pats', zipWith rebuild pats' cs)

439 where

443 where

@@ -523,7 +527,7 @@ caseGroups (v:vs) gs err = do g <- altGroups gs

523 altGroups (ConGroup _ (CConst c) args : cs)

527 altGroups (ConGroup _ (CConst c) args : cs)

524 = (:) <$> altConstGroup c args <*> altGroups cs

528 = (:) <$> altConstGroup c args <*> altGroups cs

525

529

526− altGroup n i args

530+ altGroup n i args

527 = do inacc <- inaccessibleArgs n

531 = do inacc <- inaccessibleArgs n

528 (newVars, accVars, inaccVars, nextCs) <- argsToAlt inacc args

532 (newVars, accVars, inaccVars, nextCs) <- argsToAlt inacc args

529 matchCs <- match (accVars ++ vs ++ inaccVars) nextCs err

533 matchCs <- match (accVars ++ vs ++ inaccVars) nextCs err

@@ -556,7 +560,7 @@ argsToAlt inacc rs@((r, m) : rest) = do

556 -- Create names for new variables arising from the given patterns.

560 -- Create names for new variables arising from the given patterns.

557 getNewVars :: [Pat] -> CaseBuilder [Name]

561 getNewVars :: [Pat] -> CaseBuilder [Name]

558 getNewVars [] = return []

562 getNewVars [] = return []

559− getNewVars ((PV n t) : ns) = do v <- getVar "e"

563+ getNewVars ((PV n t) : ns) = do v <- getVar "e"

560 nsv <- getNewVars ns

564 nsv <- getNewVars ns

561

565

562 -- Record the type of the variable.

566 -- Record the type of the variable.

@@ -666,6 +670,7 @@ depatt ns tm = dp [] tm

666 applyMaps ms t = t

670 applyMaps ms t = t

667

671

668-- FIXME: Do this for SucCase too

672-- FIXME: Do this for SucCase too

673+-- Issue #1719 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1719

669prune :: Bool -- ^ Convert single branches to projections (only useful at runtime)

674prune :: Bool -- ^ Convert single branches to projections (only useful at runtime)

670 -> SC -> SC

675 -> SC -> SC

671prune proj (Case up n alts) = case alts' of

676prune proj (Case up n alts) = case alts' of

@@ -689,9 +694,9 @@ prune proj (Case up n alts) = case alts' of

689 -- with sc

694 -- with sc

690 as@[ConCase cn i args sc]

695 as@[ConCase cn i args sc]

691 | proj -> let sc' = prune proj sc in

696 | proj -> let sc' = prune proj sc in

692− if any (isUsed sc') args

697+ if any (isUsed sc') args

693 then Case up n [ConCase cn i args sc']

698 then Case up n [ConCase cn i args sc']

694− else sc'

699+ else sc'

695

700

696 [SucCase cn sc]

701 [SucCase cn sc]

697 | proj

702 | proj

@@ -795,4 +800,3 @@ mkForce = mkForceSC

795 = DefaultCase (mkForceSC n arg rhs)

800 = DefaultCase (mkForceSC n arg rhs)

796

801

797 forceTm n arg t = subst n arg t

802 forceTm n arg t = subst n arg t

798−

src/Idris/Core/Constraints.hs+3−2

@@ -56,15 +56,16 @@ acyclic r cvs = checkCycle (fileFC "root") r [] 0 cvs

56 = Error $ At fc UniverseError

57 -- FIXME: Make informative

58 -- e.g. (Msg ("Cycle: " ++ show cv ++ ", " ++ show path))

59+ -- Issue #1725 on the issue tracker.

60+ -- https://github.com/idris-lang/Idris-dev/issues/1725

59 -- if we reach a cycle but we're at the same universe level, it's

61 -- if we reach a cycle but we're at the same universe level, it's

60 -- fine, because they must all be equal, so stop.

62 -- fine, because they must all be equal, so stop.

61 | inc == 0 && cv `elem` map fst path

63 | inc == 0 && cv `elem` map fst path

62 = return ()

64 = return ()

63− | otherwise

65+ | otherwise

64 = case M.lookup cv r of

66 = case M.lookup cv r of

65 Nothing -> return ()

67 Nothing -> return ()

66 Just cs -> mapM_ (next r ((cv, fc):path) inc) cs

68 Just cs -> mapM_ (next r ((cv, fc):path) inc) cs

68 next r path inc (ULT l x, fc) = check fc r path (inc + 1) x

70 next r path inc (ULT l x, fc) = check fc r path (inc + 1) x

69 next r path inc (ULE l x, fc) = check fc r path inc x

71 next r path inc (ULE l x, fc) = check fc r path inc x

70−

src/Idris/Core/Evaluate.hs+15−12

@@ -8,7 +8,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

8 Context, initContext, ctxtAlist, uconstraints, next_tvar,

9 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

10 addDatatype, addCasedef, simplifyCasedef, addOperator,

11− lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,

11+ lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,

12 lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,

13 mapDefCtxt,

14 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, isTConName, isConName, isFnName,

@@ -92,7 +92,7 @@ normaliseTrace tr ctxt env t

93-- Return a specialised name, and an updated list of reductions available,

94-- so that the caller can tell how much specialisation was achieved.

95−specialise :: Context -> Env -> [(Name, Int)] -> TT Name ->

95+specialise :: Context -> Env -> [(Name, Int)] -> TT Name ->

96 (TT Name, [(Name, Int)])

97specialise ctxt env limits t

98 = let (tm, st) =

@@ -176,7 +176,7 @@ usable False n ns

176

177

178fnCount :: Int -> Name -> Eval ()

179−fnCount inc n

179+fnCount inc n

180 = do ES ls num b <- get

181 case lookup n ls of

182 Just i -> do put $ ES ((n, (i - inc)) :

@@ -255,7 +255,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

255 ev ntimes stk top env (V i)

256 | i < length env && i >= 0 = return $ snd (env !! i)

257 | otherwise = return $ VV i

258− ev ntimes stk top env (Bind n (Let t v) sc)

258+ ev ntimes stk top env (Bind n (Let t v) sc)

259 | not runtime || occurrences n sc < 2

260 = do v' <- ev ntimes stk top env v --(finalise v)

261 sc' <- ev ntimes stk top ((n, v') : env) sc

@@ -283,7 +283,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

283 where vbind env t

284 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t

285 -- block reduction immediately under codata (and not forced)

286− ev ntimes stk top env

286+ ev ntimes stk top env

287 (App (App (App d@(P _ (UN dly) _) l@(P _ (UN lco) _)) t) arg)

288 | dly == txt "Delay" && lco == txt "LazyCodata" && not simpl

289 = do let (f, _) = unApply arg

@@ -311,7 +311,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

311 t' <- ev ntimes stk top env t

312-- tfull' <- reapply ntimes stk top env t' []

313 return (doProj t' (getValArgs t'))

314− where doProj t' (VP (DCon _ _ _) _ _, args)

314+ where doProj t' (VP (DCon _ _ _) _ _, args)

315 | i >= 0 && i < length args = args!!i

316 doProj t' _ = VProj t' i

317

@@ -338,7 +338,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

338 _ -> case args of

339 (a : as) -> return $ unload env f (a : as)

340 [] -> return f

341− reapply ntimes stk top env (VApp f a) args

341+ reapply ntimes stk top env (VApp f a) args

342 = reapply ntimes stk top env f (a : args)

343 reapply ntimes stk top env v args = return v

344

@@ -356,7 +356,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

356 do let val = lookupDefAcc n (spec || atRepl) ctxt

357 case val of

358 [(CaseOp ci _ _ _ _ cd, acc)]

359− | acc /= Frozen || sUN "assert_total" `elem` stk ->

359+ | acc /= Frozen || sUN "assert_total" `elem` stk ->

360 -- unoptimised version

361 let (ns, tree) = getCases cd in

362 if blockSimplify ci n stk

@@ -402,7 +402,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

402 t <- evTree ntimes stk top env (zip ns args') tree

403 when spec $ case t of

404 Nothing -> reinstate n -- Blocked, count n again

405− Just _ -> return ()

405+ Just _ -> return ()

406-- (zipWith (\n , t) -> (n, t)) ns args') tree

407 return (t, rest)

408 | otherwise = return (Nothing, args)

@@ -416,7 +416,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

416 (amap ++ env) etm

417 return $ Just etm'

418 evTree ntimes stk top env amap (ProjCase t alts)

419− = do t' <- ev ntimes stk top env t

419+ = do t' <- ev ntimes stk top env t

420 doCase ntimes stk top env amap t' alts

421 evTree ntimes stk top env amap (Case _ n alts)

422 = case lookup n amap of

@@ -591,10 +591,10 @@ convEq ctxt holes topx topy = ceq [] topx topy where

591 ceq ps x (Bind n (PVTy t) sc) = ceq ps x sc

592

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

594− ceq ps (V x) (P _ y _)

594+ ceq ps (V x) (P _ y _)

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

596 | otherwise = return False

597− ceq ps (P _ x _) (V y)

597+ ceq ps (P _ x _) (V y)

598 | y >= 0 && length ps > y = return (x == snd (ps!!y))

599 | otherwise = return False

600 ceq ps (Bind n xb xs) (Bind n' yb ys)

@@ -833,6 +833,9 @@ addDatatype (Data n tag ty unique cons) uctxt

833 (TyDecl (DCon tag (arity ty') unique) ty, Public, Unchecked, EmptyMI) ctxt)

834

835-- FIXME: Too many arguments! Refactor all these Bools.

836+--

837+-- Issue #1724 on the issue tracker.

838+-- https://github.com/idris-lang/Idris-dev/issues/1724

836addCasedef :: Name -> ErasureInfo -> CaseInfo ->

839addCasedef :: Name -> ErasureInfo -> CaseInfo ->

837 Bool -> Bool -> Bool -> Bool ->

840 Bool -> Bool -> Bool -> Bool ->

838 [Type] -> -- argument types

841 [Type] -> -- argument types

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

@@ -525,7 +525,6 @@ call (FFun name argTypes retType) args =

525 call' (Fun _ h) args FPtr = EPtr <$> (execIO $ callFFI h (retPtr retVoid) (prepArgs args))

526 call' (Fun _ h) args FUnit = do _ <- execIO $ callFFI h retVoid (prepArgs args)

527 return $ EP Ref unitCon EErased

528−-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)

529

528

530

529

531 prepArgs = map prepArg

530 prepArgs = map prepArg

@@ -536,6 +535,8 @@ call (FFun name argTypes retType) args =

536 prepArg (EConstant (B64 i)) = argCLong (fromIntegral i)

535 prepArg (EConstant (B64 i)) = argCLong (fromIntegral i)

537 prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)

536 prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)

538 prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars

537 prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars

538+ -- Issue #1720 on the issue tracker.

539+ -- https://github.com/idris-lang/Idris-dev/issues/1720

539 prepArg (EConstant (Str s)) = argString s

540 prepArg (EConstant (Str s)) = argString s

540 prepArg (EPtr p) = argPtr p

541 prepArg (EPtr p) = argPtr p

541 prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined

542 prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined

src/Idris/Core/ProofState.hs+16−14

@@ -151,10 +151,10 @@ match_unify' ctxt env topx topy =

151 let dont = dontunify ps

152 let inj = injective ps

153 traceWhen (unifylog ps)

154− ("Matching " ++ show (topx, topy) ++

154+ ("Matching " ++ show (topx, topy) ++

155 " in " ++ show env ++

156 "\nHoles: " ++ show (holes ps)

157− ++ "\n"

157+ ++ "\n"

158 ++ "\n" ++ show (getProofTerm (pterm ps)) ++ "\n\n"

159 ) $

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

@@ -170,7 +170,7 @@ match_unify' ctxt env topx topy =

170 return []

171-- traceWhen (unifylog ps)

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

173−-- "\nSolved: " ++ show u

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

174-- ++ "\nCurrent problems:\n" ++ qshow (problems ps)

175-- -- ++ show (pterm ps)

176-- ++ "\n----------") $

@@ -203,7 +203,7 @@ unify' ctxt env topx topy =

203 "\nHoles: " ++ show (holes ps)

204 ++ "\nInjective: " ++ show (injective ps)

205 ++ "\n") $

206− lift $ unify ctxt env topx topy inj (holes ps)

206+ lift $ unify ctxt env topx topy inj (holes ps)

207 (map fst (notunified ps)) while

208 let notu = filter (\ (n, t) -> case t of

209 P _ _ _ -> False

@@ -416,7 +416,7 @@ deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

416 Nothing -> error ("deferType can't find " ++ show n)

417

418regret :: RunTactic

419−regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =

419+regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =

420 do action (\ps -> let hs = holes ps in

421 ps { holes = hs \\ [x] })

422 return sc

@@ -495,7 +495,7 @@ solve ctxt env (Bind x (Guess ty val) sc)

495 notunified = updateNotunified [(x,val)]

496 (notunified ps),

497 instances = instances ps \\ [x] })

498− let tm' = subst x val sc in

498+ let tm' = subst x val sc in

499 return tm'

500solve _ _ h@(Bind x t sc)

501 = do ps <- get

@@ -504,7 +504,7 @@ solve _ _ h@(Bind x t sc)

504 _ -> lift $ tfail (IncompleteTerm h)

505 where findType x (Bind n (Let t v) sc)

506 = findType x v `mplus` findType x sc

507− findType x (Bind n t sc)

507+ findType x (Bind n t sc)

508 | P _ x' _ <- binderTy t, x == x' = Just n

509 | otherwise = findType x sc

510 findType x _ = Nothing

@@ -553,7 +553,7 @@ forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

553forall n ty ctxt env _ = fail "Can't pi bind here"

554

555patvar :: Name -> RunTactic

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

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

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

558 holes ps \\ [x],

559 solved = Just (x, P Bound n t),

@@ -590,7 +590,7 @@ rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =

590 [lt, l, r, p, tmv, xp]))

591 (scv, sct) <- lift $ check ctxt env sc

592 return scv

593− _ -> lift $ tfail (NotEquality tmv tmt')

593+ _ -> lift $ tfail (NotEquality tmv tmt')

594 where rname = sMN 0 "replaced"

595rewrite _ _ _ _ = fail "Can't rewrite here"

596

@@ -769,7 +769,7 @@ updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns e

769updateError [] err = err

770updateError ns (At f e) = At f (updateError ns e)

771updateError ns (Elaborating s n e) = Elaborating s n (updateError ns e)

772−updateError ns (ElaboratingArg f a env e)

772+updateError ns (ElaboratingArg f a env e)

773 = ElaboratingArg f a env (updateError ns e)

774updateError ns (CantUnify b l r e xs sc)

775 = CantUnify b (updateSolvedTerm ns l) (updateSolvedTerm ns r) (updateError ns e) xs sc

@@ -777,7 +777,7 @@ updateError ns e = e

777

778solveInProblems x val [] = []

779solveInProblems x val ((l, r, env, err) : ps)

780− = ((psubst x val l, psubst x val r,

780+ = ((psubst x val l, psubst x val r,

781 updateEnv [(x, val)] env, err) : solveInProblems x val ps)

782

783mergeNotunified :: Env -> [(Name, Term)] -> ([(Name, Term)], Fails)

@@ -785,7 +785,7 @@ mergeNotunified env ns = mnu ns [] [] where

785 mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)

786 mnu ((n, t):ns) ns_acc ps_acc

787 | Just t' <- lookup n ns, t /= t'

788− = mnu ns ((n,t') : ns_acc)

788+ = mnu ns ((n,t') : ns_acc)

789 ((t,t',env,CantUnify True t t' (Msg "") [] 0, [],Match) : ps_acc)

790 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc

791

@@ -796,6 +796,8 @@ updateNotunified ns nu = up nu where

796 ((n, t') : up nus)

797

798-- FIXME: Why not just pass the whole proof state?

799+-- Issue #1716 on the issue tracker.

800+-- https://github.com/idris-lang/Idris-dev/issues/1716

799updateProblems :: Context -> [(Name, TT Name)] -> Fails -> [Name] -> [Name] -> [Name]

801updateProblems :: Context -> [(Name, TT Name)] -> Fails -> [Name] -> [Name] -> [Name]

800 -> ([(Name, TT Name)], Fails)

802 -> ([(Name, TT Name)], Fails)

801-- updateProblems ctxt [] ps inj holes = ([], ps)

803-- updateProblems ctxt [] ps inj holes = ([], ps)

@@ -806,7 +808,7 @@ updateProblems ctxt ns ps inj holes usupp = up ns ps where

806 y' = updateSolvedTerm ns y

808 y' = updateSolvedTerm ns y

807 err' = updateError ns err

809 err' = updateError ns err

808 env' = updateEnv ns env in

810 env' = updateEnv ns env in

809−-- trace ("Updating " ++ show (x',y')) $

811+-- trace ("Updating " ++ show (x',y')) $

810 case unify ctxt env' x' y' inj holes usupp while of

812 case unify ctxt env' x' y' inj holes usupp while of

811 OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

813 OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

812 up (ns ++ v) ps

814 up (ns ++ v) ps

@@ -867,7 +869,7 @@ processTactic (Reorder n) ps

867 return (ps' { previous = Just ps, plog = "" }, plog ps')

869 return (ps' { previous = Just ps, plog = "" }, plog ps')

868processTactic (ComputeLet n) ps

870processTactic (ComputeLet n) ps

869 = return (ps { pterm = mkProofTerm $

871 = return (ps { pterm = mkProofTerm $

870− computeLet (context ps) n

872+ computeLet (context ps) n

871 (getProofTerm (pterm ps)) }, "")

873 (getProofTerm (pterm ps)) }, "")

872processTactic UnifyProblems ps

874processTactic UnifyProblems ps

873 = let (ns', probs') = updateProblems (context ps) []

875 = let (ns', probs') = updateProblems (context ps) []

src/Idris/Core/TT.hs+8−8

@@ -486,7 +486,7 @@ intTyName (ITFixed sized) = "B" ++ show (nativeTyWidth sized)

486intTyName (ITChar) = "Char"

487intTyName (ITVec ity count) = "B" ++ show (nativeTyWidth ity) ++ "x" ++ show count

488

489−data ArithTy = ATInt IntTy | ATFloat -- TODO: Float vectors

489+data ArithTy = ATInt IntTy | ATFloat -- TODO: Float vectors https://github.com/idris-lang/Idris-dev/issues/1723

490 deriving (Show, Eq, Ord)

491{-!

492deriving instance NFData IntTy

@@ -792,7 +792,7 @@ instance TermSize (TT Name) where

792 | otherwise = 1

793 termsize n (V _) = 1

794 -- for `Bind` terms, we can erroneously declare a term

795− -- "recursive => really big" if the name of the bound

795+ -- "recursive => really big" if the name of the bound

796 -- variable is the same as the name we're using

797 -- So generate a different name in that case.

798 termsize n (Bind n' (Let t v) sc)

@@ -971,19 +971,19 @@ subst n v tm = fst $ subst' 0 tm

971 subst' i t@(Bind x b sc) | x /= n

972 = let (b', ub) = substB' i b

973 (sc', usc) = subst' (i+1) sc in

974− if ub || usc then (Bind x b' sc', True) else (t, False)

974+ if ub || usc then (Bind x b' sc', True) else (t, False)

975− subst' i t@(App f a) = let (f', uf) = subst' i f

975+ subst' i t@(App f a) = let (f', uf) = subst' i f

976 (a', ua) = subst' i a in

977 if uf || ua then (App f' a', True) else (t, False)

978 subst' i t@(Proj x idx) = let (x', u) = subst' i x in

979 if u then (Proj x' idx, u) else (t, False)

980 subst' i t = (t, False)

981

982− substB' i b@(Let t v) = let (t', ut) = subst' i t

982+ substB' i b@(Let t v) = let (t', ut) = subst' i t

983 (v', uv) = subst' i v in

984 if ut || uv then (Let t' v', True)

985 else (b, False)

986− substB' i b@(Guess t v) = let (t', ut) = subst' i t

986+ substB' i b@(Guess t v) = let (t', ut) = subst' i t

987 (v', uv) = subst' i v in

988 if ut || uv then (Guess t' v', True)

989 else (b, False)

@@ -1090,7 +1090,7 @@ unList tm = case unApply tm of

1090-- Bruijn indices.

1091forget :: TT Name -> Raw

1092forget tm = forgetEnv [] tm

1093−

1093+

1094forgetEnv :: [Name] -> TT Name -> Raw

1095forgetEnv env (P _ n _) = Var n

1096forgetEnv env (V i) = Var (env !! i)

@@ -1384,7 +1384,7 @@ liftPats tm = let (tm', ps) = runState (getPats tm) [] in

1384 orderPats $ bindPats (reverse ps) tm'

1385 where

1386 bindPats [] tm = tm

1387− bindPats ((n, t):ps) tm

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

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

1389 | otherwise = bindPats ps tm

1390

src/Idris/Core/Typecheck.hs+20−18

@@ -53,7 +53,7 @@ isType ctxt env tm = isType' (normalise ctxt env tm)

53recheck :: Context -> Env -> Raw -> Term -> TC (Term, Type, UCs)

54recheck = recheck_borrowing False []

56−recheck_borrowing :: Bool -> [Name] -> Context -> Env -> Raw -> Term ->

56+recheck_borrowing :: Bool -> [Name] -> Context -> Env -> Raw -> Term ->

57 TC (Term, Type, UCs)

58recheck_borrowing uniq_check bs ctxt env tm orig

59 = let v = next_tvar ctxt in

@@ -65,7 +65,7 @@ recheck_borrowing uniq_check bs ctxt env tm orig

65 return (tm, ty, constraints)

67check :: Context -> Env -> Raw -> TC (Term, Type)

68−check ctxt env tm

68+check ctxt env tm

69 = evalStateT (check' True ctxt env tm) (0, []) -- Holes allowed

71check' :: Bool -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)

@@ -93,12 +93,12 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

93 ty@(Bind x (Pi s k) t) -> ty

94 _ -> normalise ctxt env fty

95 case fty' of

96− Bind x (Pi s k) t ->

96+ Bind x (Pi s k) t ->

97 do convertsC ctxt env aty s

98 let apty = simplify initContext env

99 (Bind x (Let aty av) t)

100 return (App fv av, apty)

101− t -> lift $ tfail $ NonFunctionType fv fty

101+ t -> lift $ tfail $ NonFunctionType fv fty

102 chk u env RType

103 | holes = return (TType (UVal 0), TType (UVal 0))

104 | otherwise = do (v, cs) <- get

@@ -107,7 +107,9 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

107 return (TType (UVar v), TType (UVar (v+1)))

108 chk u env (RUType un)

109 | holes = return (UType un, TType (UVal 0))

110− | otherwise = do -- TODO! (v, cs) <- get

110+ | otherwise = do -- TODO! Issue #1715 on the issue tracker.

111+ -- https://github.com/idris-lang/Idris-dev/issues/1715

112+ -- (v, cs) <- get

111 -- let c = ULT (UVar v) (UVar (v+1))

113 -- let c = ULT (UVar v) (UVar (v+1))

112 -- put (v+2, (c:cs))

114 -- put (v+2, (c:cs))

113 -- return (TType (UVar v), TType (UVar (v+1)))

115 -- return (TType (UVar v), TType (UVar (v+1)))

@@ -135,7 +137,6 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

135 = do (sv, st) <- chk u env s

137 = do (sv, st) <- chk u env s

136 (kv, kt) <- chk u env k

138 (kv, kt) <- chk u env k

137 (tv, tt) <- chk st ((n, Pi sv kv) : env) t

139 (tv, tt) <- chk st ((n, Pi sv kv) : env) t

138−-- let tv = mkUniquePi kv tv_in

139 (v, cs) <- get

140 (v, cs) <- get

140 case (normalise ctxt env st, normalise ctxt env tt) of

141 case (normalise ctxt env st, normalise ctxt env tt) of

141 (TType su, TType tu) -> do

142 (TType su, TType tu) -> do

@@ -148,12 +149,12 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

148 return (Bind n (Pi (uniqueBinders (map fst env) sv) k')

149 return (Bind n (Pi (uniqueBinders (map fst env) sv) k')

149 (pToV n tv), k')

150 (pToV n tv), k')

150

151

151− where mkUniquePi kv (Bind n (Pi s k) sc)

152+ where mkUniquePi kv (Bind n (Pi s k) sc)

152 = let k' = smaller kv k in

153 = let k' = smaller kv k in

153 Bind n (Pi s k') (mkUniquePi k' sc)

154 Bind n (Pi s k') (mkUniquePi k' sc)

154− mkUniquePi kv (Bind n (Lam t) sc)

155+ mkUniquePi kv (Bind n (Lam t) sc)

155 = Bind n (Lam (mkUniquePi kv t)) (mkUniquePi kv sc)

156 = Bind n (Lam (mkUniquePi kv t)) (mkUniquePi kv sc)

156− mkUniquePi kv (Bind n (Let t v) sc)

157+ mkUniquePi kv (Bind n (Let t v) sc)

157 = Bind n (Let (mkUniquePi kv t) v) (mkUniquePi kv sc)

158 = Bind n (Let (mkUniquePi kv t) v) (mkUniquePi kv sc)

158 mkUniquePi kv t = t

159 mkUniquePi kv t = t

159

160

@@ -257,9 +258,9 @@ data UniqueUse = Never -- no more times

257-- If any binders are of kind 'UniqueType' or 'AllTypes' and the name appears

258-- If any binders are of kind 'UniqueType' or 'AllTypes' and the name appears

258-- in the scope more than once, this is an error.

259-- in the scope more than once, this is an error.

259checkUnique :: [Name] -> Context -> Env -> Term -> TC ()

260checkUnique :: [Name] -> Context -> Env -> Term -> TC ()

260−checkUnique borrowed ctxt env tm

261+checkUnique borrowed ctxt env tm

261 = evalStateT (chkBinders env (explicitNames tm)) []

262 = evalStateT (chkBinders env (explicitNames tm)) []

262− where

263+ where

263 isVar (P _ _ _) = True

264 isVar (P _ _ _) = True

264 isVar (V _) = True

265 isVar (V _) = True

265 isVar _ = False

266 isVar _ = False

@@ -272,10 +273,10 @@ checkUnique borrowed ctxt env tm

272 chkBinders env (App (App (P _ (NS (UN lend) [owner]) _) t) a)

273 chkBinders env (App (App (P _ (NS (UN lend) [owner]) _) t) a)

273 | isVar a && owner == txt "Ownership" &&

274 | isVar a && owner == txt "Ownership" &&

274 (lend == txt "lend" || lend == txt "Read")

275 (lend == txt "lend" || lend == txt "Read")

275− = do chkBinders env t -- Check the type normally

276+ = do chkBinders env t -- Check the type normally

276 st <- get

277 st <- get

277 -- Remove the 'LendOnly' names from the unusable set

278 -- Remove the 'LendOnly' names from the unusable set

278− put (filter (\(n, (ok, _)) -> ok /= LendOnly) st)

279+ put (filter (\(n, (ok, _)) -> ok /= LendOnly) st)

279 chkBinders env a

280 chkBinders env a

280 put st -- Reset the old state after checking the argument

281 put st -- Reset the old state after checking the argument

281 chkBinders env (App f a) = do chkBinders env f; chkBinders env a

282 chkBinders env (App f a) = do chkBinders env f; chkBinders env a

@@ -288,14 +289,16 @@ checkUnique borrowed ctxt env tm

288 chkBinders ((n, b) : env) t

289 chkBinders ((n, b) : env) t

289 chkBinders env t = return ()

290 chkBinders env t = return ()

290

291

291− chkBinderName :: Env -> Name -> Binder Term ->

292+ chkBinderName :: Env -> Name -> Binder Term ->

292 StateT [(Name, (UniqueUse, Universe))] TC ()

293 StateT [(Name, (UniqueUse, Universe))] TC ()

293 chkBinderName env n b

294 chkBinderName env n b

294 = do let rawty = forgetEnv (map fst env) (binderTy b)

295 = do let rawty = forgetEnv (map fst env) (binderTy b)

295 (_, kind) <- lift $ check ctxt env rawty -- FIXME: Cache in binder?

296 (_, kind) <- lift $ check ctxt env rawty -- FIXME: Cache in binder?

297+ -- Issue #1714 on the issue tracker

298+ -- https://github.com/idris-lang/Idris-dev/issues/1714

296 case kind of

299 case kind of

297 UType UniqueType -> do ns <- get

300 UType UniqueType -> do ns <- get

298− if n `elem` borrowed

301+ if n `elem` borrowed

299 then put ((n, (LendOnly, NullType)) : ns)

302 then put ((n, (LendOnly, NullType)) : ns)

300 else put ((n, (Once, UniqueType)) : ns)

303 else put ((n, (Once, UniqueType)) : ns)

301 UType NullType -> do ns <- get

304 UType NullType -> do ns <- get

@@ -304,13 +307,12 @@ checkUnique borrowed ctxt env tm

304 put ((n, (Once, AllTypes)) : ns)

307 put ((n, (Once, AllTypes)) : ns)

305 _ -> return ()

308 _ -> return ()

306

309

307− chkName n

310+ chkName n

308 = do ns <- get

311 = do ns <- get

309 case lookup n ns of

312 case lookup n ns of

310 Nothing -> return ()

313 Nothing -> return ()

311 Just (Many, k) -> return ()

314 Just (Many, k) -> return ()

312 Just (Never, k) -> lift $ tfail (UniqueError k n)

315 Just (Never, k) -> lift $ tfail (UniqueError k n)

313 Just (LendOnly, k) -> lift $ tfail (UniqueError k n)

316 Just (LendOnly, k) -> lift $ tfail (UniqueError k n)

314− Just (Once, k) -> put ((n, (Never, k)) :

317+ Just (Once, k) -> put ((n, (Never, k)) :

315 filter (\x -> fst x /= n) ns)

318 filter (\x -> fst x /= n) ns)

316−

src/Idris/Core/Unify.hs+40−38

@@ -32,7 +32,7 @@ type Injs = [(TT Name, TT Name, TT Name)]

32type Fails = [(TT Name, TT Name, Env, Err, [FailContext], FailAt)]

34unrecoverable :: Fails -> Bool

35−unrecoverable = any bad

35+unrecoverable = any bad

36 where bad (_,_,_, err, _, _) = unrec err

38 unrec (CantUnify r _ _ _ _ _) = not r

@@ -92,12 +92,12 @@ match_unify ctxt env topx topy inj holes from =

92 | (P (DCon _ _ _) _ _, _) <- unApply x,

93 holeIn env f || f `elem` holes

94 = let n' = uniqueName (sMN 0 "mv") (map fst env) in

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

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

96 un names tm@(App (P _ f (Bind fn (Pi t _) sc)) a) x

97 | (P (DCon _ _ _) _ _, _) <- unApply x,

98 holeIn env f || f `elem` holes

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

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

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

101

102 un names tx@(P _ x _) tm

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

@@ -106,12 +106,12 @@ match_unify ctxt env topx topy inj holes from =

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

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

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

109− | length bnames > i,

109+ | length bnames > i,

110− fst (fst (bnames!!i)) == x ||

110+ fst (fst (bnames!!i)) == x ||

111 snd (fst (bnames!!i)) == x = do sc 1; return []

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

113 | length bnames > i,

114− fst (fst (bnames!!i)) == x ||

114+ fst (fst (bnames!!i)) == x ||

115 snd (fst (bnames!!i)) == x = do sc 1; return []

116 un bnames (Bind x bx sx) (Bind y by sy) | notHole bx && notHole by

117 = do h1 <- uB bnames bx by

@@ -124,7 +124,7 @@ match_unify ctxt env topx topy inj holes from =

124 un names x y

125 | OK True <- convEq' ctxt holes x y = do sc 1; return []

126 | otherwise = do UI s f <- get

127− let r = recoverable (normalise ctxt env x)

127+ let r = recoverable (normalise ctxt env x)

128 (normalise ctxt env y)

129 let err = cantUnify from r

130 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

@@ -139,7 +139,7 @@ match_unify ctxt env topx topy inj holes from =

139 uB bnames (Lam tx) (Lam ty) = un bnames tx ty

140 uB bnames (Pi tx _) (Pi ty _) = un bnames tx ty

141 uB bnames x y = do UI s f <- get

142− let r = recoverable (normalise ctxt env (binderTy x))

142+ let r = recoverable (normalise ctxt env (binderTy x))

143 (normalise ctxt env (binderTy y))

144 let err = cantUnify from r topx topy

145 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

@@ -152,12 +152,13 @@ match_unify ctxt env topx topy inj holes from =

152

153 -- TODO: there's an annoying amount of repetition between this and the

154 -- main unification function. Consider lifting it out.

155+ -- Issue #1721 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1721

155

156

156 sc i = do UI s f <- get

157 sc i = do UI s f <- get

157 put (UI (s+i) f)

158 put (UI (s+i) f)

158

159

159 unifyFail x y = do UI s f <- get

160 unifyFail x y = do UI s f <- get

160− let r = recoverable (normalise ctxt env x)

161+ let r = recoverable (normalise ctxt env x)

161 (normalise ctxt env y)

162 (normalise ctxt env y)

162 let err = cantUnify from r

163 let err = cantUnify from r

163 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

164 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

@@ -192,23 +193,23 @@ match_unify ctxt env topx topy inj holes from =

192 where inst [] tm = tm

193 where inst [] tm = tm

193 inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)

194 inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)

194

195

195− bind i ns tm

196+ bind i ns tm

196 | i < 0 = tm

197 | i < 0 = tm

197 | otherwise = let ((x,y),ty) = ns!!i in

198 | otherwise = let ((x,y),ty) = ns!!i in

198 App (Bind y (Lam ty) (bind (i-1) ns tm))

199 App (Bind y (Lam ty) (bind (i-1) ns tm))

199 (P Bound x ty)

200 (P Bound x ty)

200−

201+

201renameBinders env (x, t) = (x, renameBindersTm env t)

202renameBinders env (x, t) = (x, renameBindersTm env t)

202

203

203renameBindersTm :: Env -> TT Name -> TT Name

204renameBindersTm :: Env -> TT Name -> TT Name

204renameBindersTm env tm = uniqueBinders (map fst env) tm

205renameBindersTm env tm = uniqueBinders (map fst env) tm

205 where

206 where

206 uniqueBinders env (Bind n b sc)

207 uniqueBinders env (Bind n b sc)

207− | n `elem` env

208+ | n `elem` env

208 = let n' = uniqueName n env in

209 = let n' = uniqueName n env in

209 explicitHole $ Bind n' (fmap (uniqueBinders env) b)

210 explicitHole $ Bind n' (fmap (uniqueBinders env) b)

210 (uniqueBinders (n':env) (rename n n' sc))

211 (uniqueBinders (n':env) (rename n n' sc))

211− | otherwise = Bind n (fmap (uniqueBinders (n:env)) b)

212+ | otherwise = Bind n (fmap (uniqueBinders (n:env)) b)

212 (uniqueBinders (n:env) sc)

213 (uniqueBinders (n:env) sc)

213 uniqueBinders env (App f a) = App (uniqueBinders env f) (uniqueBinders env a)

214 uniqueBinders env (App f a) = App (uniqueBinders env f) (uniqueBinders env a)

214 uniqueBinders env t = t

215 uniqueBinders env t = t

@@ -218,7 +219,7 @@ renameBindersTm env tm = uniqueBinders (map fst env) tm

218 rename n n' (App f a) = App (rename n n' f) (rename n n' a)

219 rename n n' (App f a) = App (rename n n' f) (rename n n' a)

219 rename n n' t = t

220 rename n n' t = t

220

221

221− explicitHole (Bind n (Hole ty) sc)

222+ explicitHole (Bind n (Hole ty) sc)

222 = Bind n (Hole ty) (instantiate (P Bound n ty) sc)

223 = Bind n (Hole ty) (instantiate (P Bound n ty) sc)

223 explicitHole t = t

224 explicitHole t = t

224

225

@@ -227,7 +228,7 @@ trimSolutions ns = followSols (dropPairs ns)

227 dropPairs (n@(x, P _ x' _) : ns)

228 dropPairs (n@(x, P _ x' _) : ns)

228 | x == x' = dropPairs ns

229 | x == x' = dropPairs ns

229 | otherwise

230 | otherwise

230− = n : dropPairs

231+ = n : dropPairs

231 (filter (\t -> case t of

232 (filter (\t -> case t of

232 (n, P _ n' _) -> not (n == x' && n' == x)

233 (n, P _ n' _) -> not (n == x' && n' == x)

233 _ -> True) ns)

234 _ -> True) ns)

@@ -253,14 +254,14 @@ hasv (App f a) = hasv f || hasv a

253hasv (Bind x b sc) = hasv (binderTy b) || hasv sc

254hasv (Bind x b sc) = hasv (binderTy b) || hasv sc

254hasv _ = False

255hasv _ = False

255

256

256−unify :: Context -> Env -> TT Name -> TT Name ->

257+unify :: Context -> Env -> TT Name -> TT Name ->

257 [Name] -> [Name] -> [Name] -> [FailContext] ->

258 [Name] -> [Name] -> [Name] -> [FailContext] ->

258 TC ([(Name, TT Name)], Fails)

259 TC ([(Name, TT Name)], Fails)

259unify ctxt env topx topy inj holes usersupp from =

260unify ctxt env topx topy inj holes usersupp from =

260−-- traceWhen (hasv topx || hasv topy)

261+-- traceWhen (hasv topx || hasv topy)

261-- ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $

262-- ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $

262 -- don't bother if topx and topy are different at the head

263 -- don't bother if topx and topy are different at the head

263− case runStateT (un False [] (renameBindersTm env topx)

264+ case runStateT (un False [] (renameBindersTm env topx)

264 (renameBindersTm env topy)) (UI 0 []) of

265 (renameBindersTm env topy)) (UI 0 []) of

265 OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v),

266 OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v),

266 [])

267 [])

@@ -271,7 +272,7 @@ unify ctxt env topx topy inj holes usersupp from =

271 case runStateT (un False [] topxn topyn)

272 case runStateT (un False [] topxn topyn)

272 (UI 0 []) of

273 (UI 0 []) of

273 OK (v, UI _ fails) ->

274 OK (v, UI _ fails) ->

274− return (map (renameBinders env) (trimSolutions v),

275+ return (map (renameBinders env) (trimSolutions v),

275 reverse fails)

276 reverse fails)

276-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

277-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

277 Error e -> tfail e

278 Error e -> tfail e

@@ -287,8 +288,8 @@ unify ctxt env topx topy inj holes usersupp from =

287 injective (App f a) = injective f -- && injective a

288 injective (App f a) = injective f -- && injective a

288 injective _ = False

289 injective _ = False

289

290

290−-- injectiveVar (P _ (MN _ _) _) = True -- TMP HACK

291+-- injectiveVar (P _ (MN _ _) _) = True -- TMP HACK

291− injectiveVar (P _ n _) = n `elem` inj

292+ injectiveVar (P _ n _) = n `elem` inj

292 injectiveVar (App f a) = injectiveVar f -- && injective a

293 injectiveVar (App f a) = injectiveVar f -- && injective a

293 injectiveVar _ = False

294 injectiveVar _ = False

294

295

@@ -364,7 +365,7 @@ unify ctxt env topx topy inj holes usersupp from =

364 then unifyTmpFail xtm tm

365 then unifyTmpFail xtm tm

365 else do sc 1

366 else do sc 1

366 return x

367 return x

367− | pureTerm tm, not (injective xtm) && injective tm

368+ | pureTerm tm, not (injective xtm) && injective tm

368 = do checkCycle bnames (x, tm)

369 = do checkCycle bnames (x, tm)

369 unifyTmpFail xtm tm

370 unifyTmpFail xtm tm

370 un' fn bnames tm ytm@(P _ y _)

371 un' fn bnames tm ytm@(P _ y _)

@@ -378,16 +379,16 @@ unify ctxt env topx topy inj holes usersupp from =

378 then unifyTmpFail tm ytm

379 then unifyTmpFail tm ytm

379 else do sc 1

380 else do sc 1

380 return x

381 return x

381− | pureTerm tm, not (injective ytm) && injective tm

382+ | pureTerm tm, not (injective ytm) && injective tm

382 = do checkCycle bnames (y, tm)

383 = do checkCycle bnames (y, tm)

383 unifyTmpFail tm ytm

384 unifyTmpFail tm ytm

384 un' fn bnames (V i) (P _ x _)

385 un' fn bnames (V i) (P _ x _)

385 | length bnames > i,

386 | length bnames > i,

386− fst ((map fst bnames)!!i) == x ||

387+ fst ((map fst bnames)!!i) == x ||

387 snd ((map fst bnames)!!i) == x = do sc 1; return []

388 snd ((map fst bnames)!!i) == x = do sc 1; return []

388 un' fn bnames (P _ x _) (V i)

389 un' fn bnames (P _ x _) (V i)

389 | length bnames > i,

390 | length bnames > i,

390− fst ((map fst bnames)!!i) == x ||

391+ fst ((map fst bnames)!!i) == x ||

391 snd ((map fst bnames)!!i) == x = do sc 1; return []

392 snd ((map fst bnames)!!i) == x = do sc 1; return []

392

393

393 un' fn names topx@(Bind n (Hole t) sc) y = unifyTmpFail topx y

394 un' fn names topx@(Bind n (Hole t) sc) y = unifyTmpFail topx y

@@ -417,17 +418,17 @@ unify ctxt env topx topy inj holes usersupp from =

417 un' fn bnames (App f x) (Bind n (Pi t k) y)

418 un' fn bnames (App f x) (Bind n (Pi t k) y)

418 | noOccurrence n y && injectiveApp f

419 | noOccurrence n y && injectiveApp f

419 = do ux <- un' False bnames x y

420 = do ux <- un' False bnames x y

420− uf <- un' False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

421+ uf <- un' False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

421 (Bind n (Pi t k) (V 1)))

422 (Bind n (Pi t k) (V 1)))

422 combine bnames ux uf

423 combine bnames ux uf

423−

424+

424 un' fn bnames (Bind n (Pi t k) y) (App f x)

425 un' fn bnames (Bind n (Pi t k) y) (App f x)

425 | noOccurrence n y && injectiveApp f

426 | noOccurrence n y && injectiveApp f

426 = do ux <- un' False bnames y x

427 = do ux <- un' False bnames y x

427− uf <- un' False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

428+ uf <- un' False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

428 (Bind n (Pi t k) (V 1))) f

429 (Bind n (Pi t k) (V 1))) f

429 combine bnames ux uf

430 combine bnames ux uf

430−

431+

431 un' fn bnames (Bind x bx sx) (Bind y by sy)

432 un' fn bnames (Bind x bx sx) (Bind y by sy)

432 | sameBinder bx by

433 | sameBinder bx by

433 = do h1 <- uB bnames bx by

434 = do h1 <- uB bnames bx by

@@ -438,9 +439,9 @@ unify ctxt env topx topy inj holes usersupp from =

438 sameBinder _ _ = False

439 sameBinder _ _ = False

439 un' fn bnames x y

440 un' fn bnames x y

440 | OK True <- convEq' ctxt holes x y = do sc 1; return []

441 | OK True <- convEq' ctxt holes x y = do sc 1; return []

441− | isUniverse x && isUniverse y = do sc 1; return []

442+ | isUniverse x && isUniverse y = do sc 1; return []

442 | otherwise = do UI s f <- get

443 | otherwise = do UI s f <- get

443− let r = recoverable (normalise ctxt env x)

444+ let r = recoverable (normalise ctxt env x)

444 (normalise ctxt env y)

445 (normalise ctxt env y)

445 let err = cantUnify from r

446 let err = cantUnify from r

446 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

447 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

@@ -519,7 +520,7 @@ unify ctxt env topx topy inj holes usersupp from =

519 _ -> False

520 _ -> False

520

521

521 metavar t = case t of

522 metavar t = case t of

522− P _ x _ -> (x `notElem` usersupp &&

523+ P _ x _ -> (x `notElem` usersupp &&

523 (x `elem` holes || holeIn env x))

524 (x `elem` holes || holeIn env x))

524 || globmetavar t

525 || globmetavar t

525 _ -> False

526 _ -> False

@@ -566,7 +567,7 @@ unify ctxt env topx topy inj holes usersupp from =

566 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty

567 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty

567 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty

568 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty

568 uB bnames x y = do UI s f <- get

569 uB bnames x y = do UI s f <- get

569− let r = recoverable (normalise ctxt env (binderTy x))

570+ let r = recoverable (normalise ctxt env (binderTy x))

570 (normalise ctxt env (binderTy y))

571 (normalise ctxt env (binderTy y))

571 let err = cantUnify from r topx topy

572 let err = cantUnify from r topx topy

572 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

573 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

@@ -590,9 +591,9 @@ unify ctxt env topx topy inj holes usersupp from =

590 else return [(x, bind v ns tm)]

591 else return [(x, bind v ns tm)]

591 where inst [] tm = tm

592 where inst [] tm = tm

592 inst (((n, _), _) : ns) tm = inst ns (substV (P Bound n Erased) tm)

593 inst (((n, _), _) : ns) tm = inst ns (substV (P Bound n Erased) tm)

593− checkScope ns (x, tm) = lift $ tfail (Msg "HOLE ERROR")

594+ checkScope ns (x, tm) = lift $ tfail (Msg "HOLE ERROR")

594

595

595− bind i ns tm

596+ bind i ns tm

596 | i < 0 = tm

597 | i < 0 = tm

597 | otherwise = let ((x,y),ty) = ns!!i in

598 | otherwise = let ((x,y),ty) = ns!!i in

598 App (Bind y (Lam ty) (bind (i-1) ns tm))

599 App (Bind y (Lam ty) (bind (i-1) ns tm))

@@ -639,7 +640,9 @@ envPos x i ((y, _) : ys) | x == y = i

639-- FIXME: Depending on how overloading gets used, this may cause problems. Better

640-- FIXME: Depending on how overloading gets used, this may cause problems. Better

640-- rethink overloading properly...

641-- rethink overloading properly...

641-- ASSUMPTION: inputs are in normal form

642-- ASSUMPTION: inputs are in normal form

642−

643+--

644+-- Issue #1722 on the issue tracker https://github.com/idris-lang/Idris-dev/issues/1722

645+--

643recoverable t@(App _ _) _

646recoverable t@(App _ _) _

644 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False

647 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False

645recoverable _ t@(App _ _)

648recoverable _ t@(App _ _)

@@ -658,7 +661,7 @@ recoverable (App f a) p@(Constant _) = recoverable f p

658recoverable p@(P _ n _) (App f a) = recoverable p f

661recoverable p@(P _ n _) (App f a) = recoverable p f

659recoverable (App f a) p@(P _ _ _) = recoverable f p

662recoverable (App f a) p@(P _ _ _) = recoverable f p

660recoverable (App f a) (App f' a')

663recoverable (App f a) (App f' a')

661− | f == f' = recoverable a a'

664+ | f == f' = recoverable a a'

662recoverable (App f a) (App f' a')

665recoverable (App f a) (App f' a')

663 = recoverable f f' -- && recoverable a a'

666 = recoverable f f' -- && recoverable a a'

664recoverable f (Bind _ (Pi _ _) sc)

667recoverable f (Bind _ (Pi _ _) sc)

@@ -685,4 +688,3 @@ patIn env n = case lookup n env of

685 Just (PVar _) -> True

688 Just (PVar _) -> True

686 Just (PVTy _) -> True

689 Just (PVTy _) -> True

687 _ -> False

690 _ -> False

688−