git.iko.soy/Idris-dev
on master help sign in
Add regression test for #3651.
3f0d399Ryan Scott
src/Idris/Elab/Term.hs+2−2
compare with master
unifiedsplit
@@ -1522,7 +1522,7 @@ elab ist info emode opts fn tm
1522 (arg, x : rest)
1522 (arg, x : rest)
1523
1523
1524 insertScopedImps :: FC -> Name -> [Name] -> Type -> [PArg] -> ElabD [PArg]
1524 insertScopedImps :: FC -> Name -> [Name] -> Type -> [PArg] -> ElabD [PArg]
1525− insertScopedImps fc f knowns ty xs =
1525+ insertScopedImps fc f knowns ty xs =
1526 do mapM_ (checkKnownImplicit (map fst (getArgTys ty) ++ knowns)) xs
1526 do mapM_ (checkKnownImplicit (map fst (getArgTys ty) ++ knowns)) xs
1527 doInsert ty xs
1527 doInsert ty xs
1528 where
1528 where
@@ -1538,7 +1538,7 @@ elab ist info emode opts fn tm
1538 = liftM (x :) (doInsert sc xs)
1538 = liftM (x :) (doInsert sc xs)
1539 doInsert ty xs = return xs
1539 doInsert ty xs = return xs
1540
1540
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
1542 -- scoped implicit or a top level implicit, otherwise report an error
1542 -- scoped implicit or a top level implicit, otherwise report an error
1543 checkKnownImplicit ns imp@(PImp{})
1543 checkKnownImplicit ns imp@(PImp{})
1544 | pname imp `elem` ns = return ()
1544 | pname imp `elem` ns = return ()
test/TestData.hs+2−1
@@ -245,7 +245,8 @@ testFamiliesData = [
245 ( 52, C_CG ),
245 ( 52, C_CG ),
246 ( 67, ANY ),
246 ( 67, ANY ),
247 ( 75, ANY ),
247 ( 75, ANY ),
248− ( 76, ANY )]),
248+ ( 76, ANY ),
249+ ( 77, ANY )]),
249 ("regression", "Regression",
250 ("regression", "Regression",
250 [ ( 1 , ANY ),
251 [ ( 1 , ANY ),
251 ( 2 , ANY )]),
252 ( 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