Fix parameter propagation error
This catches the most blatant attempts at typecase, but there are still
a couple of other sneaky tricks that will get past the checker.
commit957dd616c23b00926e8cb3f6e64d21e570a3b0ae
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateFri 19 Dec 2014, 00:38 (12 years ago)
parenta427f21
src/Idris/Elab/Utils.hs+3
@@ -157,6 +157,9 @@ pvars ist _ = []
157157getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t _) sc)
158158 = nub $ getFixedInType i env [] t ++
159159 getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
160+ ++ case t of
161+ P _ n _ -> if n `elem` env then [n] else []
162+ _ -> []
160163getFixedInType i env (_ : is) (Bind n (Pi t _) sc)
161164 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
162165getFixedInType i env is tm@(App f a)