on master help sign in
Normalise local variable types in metavariables
bf52728Edwin Brady
src/Idris/Elab/Term.hs+2−2
@@ -1818,12 +1818,12 @@ collectDeferred top casenames ctxt (Bind n (GHole i t) app) =
1818 tidy ctxt env t | (f, args) <- unApply t,
1818 tidy ctxt env t | (f, args) <- unApply t,
1819 P _ specn _ <- getFn f,
1819 P _ specn _ <- getFn f,
1820 n `notElem` casenames
1820 n `notElem` casenames
1821− = fst $ specialise ctxt env [(specn, 99999)] t
1821+ = normalise ctxt env t
1822 tidy ctxt env t@(Bind n (Let _ _) sct)
1822 tidy ctxt env t@(Bind n (Let _ _) sct)
1823 | (f, args) <- unApply sct,
1823 | (f, args) <- unApply sct,
1824 P _ specn _ <- getFn f,
1824 P _ specn _ <- getFn f,
1825 n `notElem` casenames
1825 n `notElem` casenames
1826− = fst $ specialise ctxt env [(specn, 99999)] t
1826+ = normalise ctxt env t
1827 tidy ctxt env t = t
1827 tidy ctxt env t = t
1828
1828
1829 getFn (Bind n (Lam _) t) = getFn t
1829 getFn (Bind n (Lam _) t) = getFn t