git.iko.soy/Idris-dev
on master help sign in
Add regression test for #3651.

Resolves #3651.

commit3f0d39910eefd2fdadcae8fef5c71fd114a979f3 authorRyan Scott <ryan.gl.scott@gmail.com> dateThu 16 Mar 2017, 12:21 (10 years ago) parentc5be396
5 files changed+24−3
compare with master
unifiedsplit
src/Idris/Elab/Term.hs+2−2 test/TestData.hs+2−1 test/reg077/expected test/reg077/reg077.idr+17 test/reg077/run+3
src/Idris/Elab/Term.hs+2−2
@@ -1522,7 +1522,7 @@ elab ist info emode opts fn tm
15221522 (arg, x : rest)
15231523
15241524 insertScopedImps :: FC -> Name -> [Name] -> Type -> [PArg] -> ElabD [PArg]
1525− insertScopedImps fc f knowns ty xs =
1525+ insertScopedImps fc f knowns ty xs =
15261526 do mapM_ (checkKnownImplicit (map fst (getArgTys ty) ++ knowns)) xs
15271527 doInsert ty xs
15281528 where
@@ -1538,7 +1538,7 @@ elab ist info emode opts fn tm
15381538 = liftM (x :) (doInsert sc xs)
15391539 doInsert ty xs = return xs
15401540
1541− -- Any implicit in the application needs to have the name of a
1541+ -- Any implicit in the application needs to have the name of a
15421542 -- scoped implicit or a top level implicit, otherwise report an error
15431543 checkKnownImplicit ns imp@(PImp{})
15441544 | pname imp `elem` ns = return ()
test/TestData.hs+2−1
@@ -245,7 +245,8 @@ testFamiliesData = [
245245 ( 52, C_CG ),
246246 ( 67, ANY ),
247247 ( 75, ANY ),
248− ( 76, ANY )]),
248+ ( 76, ANY ),
249+ ( 77, ANY )]),
249250 ("regression", "Regression",
250251 [ ( 1 , ANY ),
251252 ( 2 , ANY )]),
test/reg077/expectednew file

No changes to the content.

test/reg077/reg077.idrnew file+17
@@ -0,0 +1,17 @@
1+data Tag : String -> List String -> Type where
2+ TZ : Tag l (l :: e)
3+ TS : Tag l e -> Tag l (l' :: e)
4+
5+SPi : (e : List String)
6+ -> ((l : String) -> Tag l e -> Type)
7+ -> Type
8+SPi [] _ = ()
9+SPi (l :: e) prop = (prop l TZ, SPi e $ \l' => \t => prop l' $ TS t)
10+
11+switch : (e : List String)
12+ -> (prop : (l : String) -> (t : Tag l e) -> Type)
13+ -> SPi e prop
14+ -> (l' : String) -> (t' : Tag l' e) -> prop l' t'
15+switch (l' :: e) prop ((propz, props)) l' TZ = propz
16+switch (l :: e) prop ((propz, props)) l' (TS t') =
17+ switch e (\l => \t => prop l (TS t)) props l' t'
test/reg077/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ --check reg077.idr
3+rm -f reg077 *.ibc