git.iko.soy/Idris-dev
on master help sign in
Fix regression with implicits, add a test

This was due to the previous erasure fix, which is now handled a different way, leaving pattern types in unnormalised form during typechecking to give unification/matching more to work with.

commitcc48d31215251b888d9ca588ac6e7cc3202c7a6d authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 11 Nov 2013, 15:28 (13 years ago) parent16eee46
5 files changed+33−6
compare with master
unifiedsplit
src/Core/Typecheck.hs+2−2 src/Idris/ElabDecls.hs+14−4 test/reg026/expected test/reg026/reg026.idr+14 test/reg026/run+3
src/Core/Typecheck.hs+2−2
@@ -188,13 +188,13 @@ check' holes ctxt env top = chk env top where
188188 lift $ isType ctxt env tt'
189189 -- Normalised version, for erasure purposes (it's easier
190190 -- to tell if it's a collapsible variable)
191− return (PVar tv')
191+ return (PVar tv)
192192 checkBinder (PVTy t)
193193 = do (tv, tt) <- chk env t
194194 let tv' = normalise ctxt env tv
195195 let tt' = normalise ctxt env tt
196196 lift $ isType ctxt env tt'
197− return (PVTy tv')
197+ return (PVTy tv)
198198
199199 discharge n (Lam t) scv sct
200200 = 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
572572 putIState (ist { idris_optimisation = opts })
573573 addIBC (IBCOpt n)
574574 ist <- getIState
575− let pats = doTransforms ist pats_in
575+ let pats = map (simple_lhs (tt_ctxt ist)) $ doTransforms ist pats_in
576576
577577 -- logLvl 3 (showSep "\n" (map (\ (l,r) ->
578578 -- show l ++ " = " ++
@@ -591,7 +591,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
591591 -- pdef is the compile-time pattern definition.
592592 -- This will get further optimised for run-time, and, separately,
593593 -- 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
595595
596596 logLvl 5 $ "Initial typechecked patterns:\n" ++ show pats
597597 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
628628 Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats
629629 _ -> return ()
630630
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
632632 tree@(CaseDef scargs sc _) <- tclift $
633633 simpleCase tcase False reflect CompileTime fc pdef
634634 cov <- coverage
@@ -737,11 +737,21 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
737737
738738 getLHS (_, l, _) = l
739739
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)
741742 simple_lhs ctxt t = t
742743
743744 simple_rt ctxt (p, x, y) = (p, x, rt_simplify ctxt [] y)
744745
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+
745755 specNames [] = Nothing
746756 specNames (Specialise ns : _) = Just ns
747757 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