git.iko.soy/Idris-dev
on master help sign in
Fix regression with implicits, add a test
cc48d31Edwin Brady
src/Core/Typecheck.hs+2−2
compare with master
unifiedsplit
@@ -188,13 +188,13 @@ check' holes ctxt env top = chk env top where
188 lift $ isType ctxt env tt'
188 lift $ isType ctxt env tt'
189 -- Normalised version, for erasure purposes (it's easier
189 -- Normalised version, for erasure purposes (it's easier
190 -- to tell if it's a collapsible variable)
190 -- to tell if it's a collapsible variable)
191− return (PVar tv')
191+ return (PVar tv)
192 checkBinder (PVTy t)
192 checkBinder (PVTy t)
193 = do (tv, tt) <- chk env t
193 = do (tv, tt) <- chk env t
194 let tv' = normalise ctxt env tv
194 let tv' = normalise ctxt env tv
195 let tt' = normalise ctxt env tt
195 let tt' = normalise ctxt env tt
196 lift $ isType ctxt env tt'
196 lift $ isType ctxt env tt'
197− return (PVTy tv')
197+ return (PVTy tv)
198
198
199 discharge n (Lam t) scv sct
199 discharge n (Lam t) scv sct
200 = return (Bind n (Lam t) scv, Bind n (Pi t) sct)
200 = return (Bind n (Lam t) scv, Bind n (Pi t) sct)
src/Idris/ElabDecls.hs+14−4
@@ -572,7 +572,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
572 putIState (ist { idris_optimisation = opts })
572 putIState (ist { idris_optimisation = opts })
573 addIBC (IBCOpt n)
573 addIBC (IBCOpt n)
574 ist <- getIState
574 ist <- getIState
575− let pats = doTransforms ist pats_in
575+ let pats = map (simple_lhs (tt_ctxt ist)) $ doTransforms ist pats_in
576
576
577 -- logLvl 3 (showSep "\n" (map (\ (l,r) ->
577 -- logLvl 3 (showSep "\n" (map (\ (l,r) ->
578 -- show l ++ " = " ++
578 -- show l ++ " = " ++
@@ -591,7 +591,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
591 -- pdef is the compile-time pattern definition.
591 -- pdef is the compile-time pattern definition.
592 -- This will get further optimised for run-time, and, separately,
592 -- This will get further optimised for run-time, and, separately,
593 -- further inlined to help with totality checking.
593 -- further inlined to help with totality checking.
594− let pdef = map debind $ map (simple_lhs (tt_ctxt ist)) pats
594+ let pdef = map debind pats
595
595
596 logLvl 5 $ "Initial typechecked patterns:\n" ++ show pats
596 logLvl 5 $ "Initial typechecked patterns:\n" ++ show pats
597 logLvl 5 $ "Initial typechecked pattern def:\n" ++ show pdef
597 logLvl 5 $ "Initial typechecked pattern def:\n" ++ show pdef
@@ -628,7 +628,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
628 Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats
628 Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats
629 _ -> return ()
629 _ -> return ()
630
630
631− let optpdef = map debind $ map (simple_lhs (tt_ctxt ist)) optpats
631+ let optpdef = map debind optpats -- $ map (simple_lhs (tt_ctxt ist)) optpats
632 tree@(CaseDef scargs sc _) <- tclift $
632 tree@(CaseDef scargs sc _) <- tclift $
633 simpleCase tcase False reflect CompileTime fc pdef
633 simpleCase tcase False reflect CompileTime fc pdef
634 cov <- coverage
634 cov <- coverage
@@ -737,11 +737,21 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
737
737
738 getLHS (_, l, _) = l
738 getLHS (_, l, _) = l
739
739
740− simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)
740+ simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x,
741+ normalisePats ctxt [] y)
741 simple_lhs ctxt t = t
742 simple_lhs ctxt t = t
742
743
743 simple_rt ctxt (p, x, y) = (p, x, rt_simplify ctxt [] y)
744 simple_rt ctxt (p, x, y) = (p, x, rt_simplify ctxt [] y)
744
745
746+ -- this is so pattern types are in the right form for erasure
747+ normalisePats ctxt env (Bind n (PVar t) sc)
748+ = let t' = normalise ctxt env t in
749+ Bind n (PVar t') (normalisePats ctxt ((n, PVar t') : env) sc)
750+ normalisePats ctxt env (Bind n (PVTy t) sc)
751+ = let t' = normalise ctxt env t in
752+ Bind n (PVTy t') (normalisePats ctxt ((n, PVar t') : env) sc)
753+ normalisePats ctxt env t = t
754+
745 specNames [] = Nothing
755 specNames [] = Nothing
746 specNames (Specialise ns : _) = Just ns
756 specNames (Specialise ns : _) = Just ns
747 specNames (_ : xs) = specNames xs
757 specNames (_ : xs) = specNames xs
test/reg026/expectednew file

No changes to the content.

test/reg026/reg026.idrnew file+14
@@ -0,0 +1,14 @@
1+module Test
2+
3+X : Nat -> Type
4+X t = (c : Nat ** so (c < 5))
5+
6+column : X t -> Nat
7+column = getWitness
8+
9+data Action = Left | Ahead | Right
10+
11+admissible : X t -> Action -> Bool
12+admissible x Ahead = column x == 0 || column x == 4
13+admissible x Left = column x <= 2
14+admissible x Right = column x >= 2
test/reg026/runnew file+3
@@ -0,0 +1,3 @@
1+#!/bin/bash
2+idris $@ reg026.idr --check reg026
3+rm -f *.ibc