ca684b6 · Idris-dev · git.iko.soy

src/Core/ProofState.hs+2−1

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

358 -- dontunify = dontunify ps \\ [x],

359 -- unified = (uh, uns ++ [(x, val)]),

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

361− return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)

361+ return $ {- Bind x (Let ty val) sc -}

362+ instantiate val (pToV x sc)

362 | otherwise = lift $ tfail $ IncompleteTerm val

363 | otherwise = lift $ tfail $ IncompleteTerm val

363solve _ _ h = do ps <- get

364solve _ _ h = do ps <- get

364 fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)

365 fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)

src/Core/TT.hs+3−1

@@ -515,7 +515,9 @@ pToV :: Eq n => n -> TT n -> TT n

515pToV n = pToV' n 0

516pToV' n i (P _ x _) | n == x = V i

517pToV' n i (Bind x b sc)

518+-- We can assume the inner scope has been pToVed already, so continue to

519+-- resolve names from the *outer* scope which may happen to have the same id.

518− | n == x = Bind x (fmap (pToV' n i) b) sc

520+-- | n == x = Bind x (fmap (pToV' n i) b) sc

519 | otherwise = Bind x (fmap (pToV' n i) b) (pToV' n (i+1) sc)

521 | otherwise = Bind x (fmap (pToV' n i) b) (pToV' n (i+1) sc)

520pToV' n i (App f a) = App (pToV' n i f) (pToV' n i a)

522pToV' n i (App f a) = App (pToV' n i f) (pToV' n i a)

521pToV' n i (Proj t idx) = Proj (pToV' n i t) idx

523pToV' n i (Proj t idx) = Proj (pToV' n i t) idx

src/Idris/ElabDecls.hs+2−1

@@ -57,7 +57,8 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

57 ctxt <- getContext

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

59 addStatics n cty ty'

60+ logLvl 6 $ "Elaborated to " ++ showEnvDbg [] tyT

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

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

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

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

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

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

63 let nty' = normalise ctxt [] nty

64 let nty' = normalise ctxt [] nty