c729d2f · Idris-dev · git.iko.soy

CHANGELOG+3

compare with master

unifiedsplit

@@ -2,6 +2,9 @@ New in 0.9.16:

2--------------

3* Inductive-inductive definitions are now supported (i.e. simultaneously

4 defined types where one is indexed by the other.)

5+* Implicits and type class constraints can now appear in scopes other than

6+ the top level.

7+* Implicits can be written {x,y,z} instead of {x,y,z : _}

5* Importing a module no longer means it is automatically reexported. A new

8* Importing a module no longer means it is automatically reexported. A new

6 "public" modifier has been added to import statements, which will reexport

9 "public" modifier has been added to import statements, which will reexport

7 the names exported from that module.

10 the names exported from that module.

idris.cabal+3

@@ -321,6 +321,9 @@ Extra-source-files:

321 test/basic011/run

322 test/basic011/*.idr

323 test/basic011/expected

324+ test/basic012/run

325+ test/basic012/*.idr

326+ test/basic012/expected

324

327

325 test/buffer001-disabled/*.idr

328 test/buffer001-disabled/*.idr

326 test/buffer001-disabled/run

329 test/buffer001-disabled/run

src/Idris/AbsSyntax.hs+5−5

@@ -1242,7 +1242,7 @@ addUsingImpls syn n fc t

1242 -- if all of args in ns, then add it

1243 doAdd (UImplicit n ty : cs) ns t

1244 | elem n ns

1245− = PPi (Imp [] Dynamic False False) n ty (doAdd cs ns t)

1245+ = PPi (Imp [] Dynamic False Nothing) n ty (doAdd cs ns t)

1246 | otherwise = doAdd cs ns t

1247

1248 -- bind the free names which weren't in the using block

@@ -1250,7 +1250,7 @@ addUsingImpls syn n fc t

1250 bindFree (n:ns) tm

1251 | elem n (map iname uimpls) = bindFree ns tm

1252 | otherwise

1253− = PPi (Imp [] Dynamic False False) n Placeholder (bindFree ns tm)

1253+ = PPi (Imp [] Dynamic False Nothing) n Placeholder (bindFree ns tm)

1254

1255 getArgnames (PPi _ n c sc)

1256 = n : getArgnames sc

@@ -1265,7 +1265,7 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)

1265 = (n, (p, t)) : collectImps sc

1266 collectImps _ = []

1267

1268− getImps (Bind n (Pi True _ _) sc) imps = getImps sc imps

1268+ getImps (Bind n (Pi (Just _) _ _) sc) imps = getImps sc imps

1269 getImps (Bind n (Pi _ t _) sc) imps

1270 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps

1271 where

@@ -1427,8 +1427,8 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1427 pibind using [] sc = sc

1428 pibind using (n:ns) sc

1429 = case lookup n using of

1430− Just ty -> PPi (Imp [] Dynamic False False) n ty (pibind using ns sc)

1430+ Just ty -> PPi (Imp [] Dynamic False Nothing) n ty (pibind using ns sc)

1431− Nothing -> PPi (Imp [] Dynamic False False) n Placeholder

1431+ Nothing -> PPi (Imp [] Dynamic False Nothing) n Placeholder

1432 (pibind using ns sc)

1433

1434-- Add implicit arguments in function calls

src/Idris/AbsSyntaxTree.hs+7−6

@@ -489,7 +489,7 @@ deriving instance NFData Static

489data Plicity = Imp { pargopts :: [ArgOpt],

490 pstatic :: Static,

491 pparam :: Bool,

492− pscoped :: Bool -- forall bound

492+ pscoped :: Maybe ImplicitInfo -- Nothing, if top level

493 }

494 | Exp { pargopts :: [ArgOpt],

495 pstatic :: Static,

@@ -506,12 +506,13 @@ deriving instance Binary Plicity

506deriving instance NFData Plicity

507!-}

508

509−is_scoped :: Plicity -> Bool

509+is_scoped :: Plicity -> Maybe ImplicitInfo

510is_scoped (Imp _ _ _ s) = s

511−is_scoped _ = False

511+is_scoped _ = Nothing

512

513−impl = Imp [] Dynamic False False

513+impl = Imp [] Dynamic False Nothing

514−forall_imp = Imp [] Dynamic False True

514+forall_imp = Imp [] Dynamic False (Just (Impl False))

515+forall_constraint = Imp [] Dynamic False (Just (Impl True))

515expl = Exp [] Dynamic False

516expl = Exp [] Dynamic False

516expl_param = Exp [] Dynamic True

517expl_param = Exp [] Dynamic True

517constraint = Constraint [] Static

518constraint = Constraint [] Static

@@ -1147,7 +1148,7 @@ getInferTerm (App (App _ _) tm) = tm

1147getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)

1148getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)

1148

1149

1149getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc

1150getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc

1150− where toTy (Lam t) = Pi False t (TType (UVar 0))

1151+ where toTy (Lam t) = Pi Nothing t (TType (UVar 0))

1151 toTy (PVar t) = PVTy t

1152 toTy (PVar t) = PVTy t

1152 toTy b = b

1153 toTy b = b

1153getInferType (App (App _ ty) _) = ty

1154getInferType (App (App _ ty) _) = ty

src/Idris/Core/Binary.hs+7

@@ -403,6 +403,13 @@ instance Binary Raw where

403 return (RUType x1)

404 _ -> error "Corrupted binary data for Raw"

405

406+instance Binary ImplicitInfo where

407+ put x

408+ = case x of

409+ Impl x1 -> put x1

410+ get

411+ = do x1 <- get

412+ return (Impl x1)

406

413

407instance (Binary b) => Binary (Binder b) where

414instance (Binary b) => Binary (Binder b) where

408 put x

415 put x

src/Idris/Core/DeepSeq.hs+3

@@ -89,6 +89,9 @@ instance NFData Err where

89 rnf (ProviderError x1) = rnf x1 `seq` ()

90 rnf (LoadingFailed x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

91

92+instance NFData ImplicitInfo where

93+ rnf (Impl x1) = rnf x1 `seq` ()

94+

92instance (NFData b) => NFData (Binder b) where

95instance (NFData b) => NFData (Binder b) where

93 rnf (Lam x1) = rnf x1 `seq` ()

96 rnf (Lam x1) = rnf x1 `seq` ()

94 rnf (Pi x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

97 rnf (Pi x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

src/Idris/Core/Elaborate.hs+4−4

@@ -369,7 +369,7 @@ intro n = processTactic' (Intro n)

369introTy :: Raw -> Maybe Name -> Elab' aux ()

370introTy ty n = processTactic' (IntroTy ty n)

371

372−forall :: Name -> Bool -> Raw -> Elab' aux ()

372+forall :: Name -> Maybe ImplicitInfo -> Raw -> Elab' aux ()

373forall n i t = processTactic' (Forall n i t)

374

375letbind :: Name -> Raw -> Raw -> Elab' aux ()

@@ -660,7 +660,7 @@ checkPiGoal n

660 f <- getNameFrom (sMN 0 "pf")

661 claim a RType

662 claim b RType

663− claim f (RBind n (Pi False (Var a) RType) (Var b))

663+ claim f (RBind n (Pi Nothing (Var a) RType) (Var b))

664 movelast a

665 movelast b

666 fill (Var f)

@@ -675,7 +675,7 @@ simple_app fun arg appstr =

675 s <- getNameFrom (sMN 0 "s")

676 claim a RType

677 claim b RType

678− claim f (RBind (sMN 0 "aX") (Pi False (Var a) RType) (Var b))

678+ claim f (RBind (sMN 0 "aX") (Pi Nothing (Var a) RType) (Var b))

679 tm <- get_term

680 start_unify s

681 claim s (Var a)

@@ -698,7 +698,7 @@ simple_app fun arg appstr =

698

699-- Abstract over an argument of unknown type, giving a name for the hole

700-- which we'll fill with the argument type too.

701−arg :: Name -> Bool -> Name -> Elab' aux ()

701+arg :: Name -> Maybe ImplicitInfo -> Name -> Elab' aux ()

702arg n i tyhole = do ty <- unique_hole tyhole

703 claim ty RType

704 movelast ty

src/Idris/Core/ProofState.hs+3−3

@@ -69,7 +69,7 @@ data Tactic = Attack

69 | CheckIn Raw

70 | Intro (Maybe Name)

71 | IntroTy Raw (Maybe Name)

72− | Forall Name Bool Raw

72+ | Forall Name (Maybe ImplicitInfo) Raw

73 | LetBind Name Raw Raw

74 | ExpandLet Name Term

75 | Rewrite Raw

@@ -412,7 +412,7 @@ defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

412 (mkApp (P Ref n ty) (map getP (reverse env'))))

413 where

414 mkTy [] t = t

415− mkTy ((n,b) : bs) t = Bind n (Pi False (binderTy b) (TType (UVar 0))) (mkTy bs t)

415+ mkTy ((n,b) : bs) t = Bind n (Pi Nothing (binderTy b) (TType (UVar 0))) (mkTy bs t)

416

417 getP (n, b) = P Bound n (binderTy b)

418

@@ -569,7 +569,7 @@ intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

569 _ -> lift $ tfail $ CantIntroduce t'

570intro n ctxt env _ = fail "Can't introduce here."

571

572−forall :: Name -> Bool -> Raw -> RunTactic

572+forall :: Name -> Maybe ImplicitInfo -> Raw -> RunTactic

573forall n impl ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

574 do (tyv, tyt) <- lift $ check ctxt env ty

575 unify' ctxt env tyt (TType (UVar 0))

src/Idris/Core/TT.hs+9−1

@@ -672,6 +672,14 @@ deriving instance Binary Raw

672deriving instance NFData Raw

673!-}

674

675+data ImplicitInfo = Impl { tcinstance :: Bool }

676+ deriving (Show, Eq, Ord)

677+

678+{-!

679+deriving instance Binary ImplicitInfo

680+deriving instance NFData ImplicitInfo

681+!-}

682+

675-- The type parameter `b` will normally be something like `TT Name` or just

683-- The type parameter `b` will normally be something like `TT Name` or just

676-- `Raw`. We do not make a type-level distinction between TT terms that happen

684-- `Raw`. We do not make a type-level distinction between TT terms that happen

677-- to be TT types and TT terms that are not TT types.

685-- to be TT types and TT terms that are not TT types.

@@ -679,7 +687,7 @@ deriving instance NFData Raw

679-- the types of bindings (and their values, if any); the attached identifiers are part

687-- the types of bindings (and their values, if any); the attached identifiers are part

680-- of the 'Bind' constructor for the 'TT' type.

688-- of the 'Bind' constructor for the 'TT' type.

681data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}}

689data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}}

682− | Pi { binderImpl :: Bool,

690+ | Pi { binderImpl :: Maybe ImplicitInfo,

683 binderTy :: !b,

691 binderTy :: !b,

684 binderKind :: !b }

692 binderKind :: !b }

685 {-^ A binding that occurs in a function type expression, e.g. @(x:Int) -> ...@

693 {-^ A binding that occurs in a function type expression, e.g. @(x:Int) -> ...@

src/Idris/Core/Typecheck.hs+1−1

@@ -230,7 +230,7 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

230 return (PVTy tv, tt')

231

232 discharge n (Lam t) bt scv sct

233− = return (Bind n (Lam t) scv, Bind n (Pi False t bt) sct)

233+ = return (Bind n (Lam t) scv, Bind n (Pi Nothing t bt) sct)

234 discharge n (Pi i t k) bt scv sct

235 = return (Bind n (Pi i t k) scv, sct)

236 discharge n (Let t v) bt scv sct

src/Idris/Delaborate.hs+6−3

@@ -57,10 +57,13 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

57 _ -> PRef un n

58 de env _ (Bind n (Lam ty) sc)

59 = PLam un n (de env [] ty) (de ((n,n):env) [] sc)

60− de env is (Bind n (Pi True ty _) sc)

60+ de env is (Bind n (Pi (Just impl) ty _) sc)

61+ | tcinstance impl

62+ = PPi constraint n (de env [] ty) (de ((n,n):env) is sc)

63+ | otherwise

61− = PPi (Imp [] Dynamic False True) n (de env [] ty) (de ((n,n):env) is sc)

64+ = PPi (Imp [] Dynamic False (Just impl)) n (de env [] ty) (de ((n,n):env) is sc)

62 de env ((PImp { argopts = opts }):is) (Bind n (Pi _ ty _) sc)

65 de env ((PImp { argopts = opts }):is) (Bind n (Pi _ ty _) sc)

63− = PPi (Imp opts Dynamic False False) n (de env [] ty) (de ((n,n):env) is sc)

66+ = PPi (Imp opts Dynamic False Nothing) n (de env [] ty) (de ((n,n):env) is sc)

64 de env (PConstraint _ _ _ _:is) (Bind n (Pi _ ty _) sc)

67 de env (PConstraint _ _ _ _:is) (Bind n (Pi _ ty _) sc)

65 = PPi constraint n (de env [] ty) (de ((n,n):env) is sc)

68 = PPi constraint n (de env [] ty) (de ((n,n):env) is sc)

66 de env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi _ ty _) sc)

69 de env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi _ ty _) sc)

src/Idris/Elab/Class.hs+1−1

@@ -134,7 +134,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

134 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

135 return ( (n, (toExp (map fst ps) Exp t')),

136 (n, (doc, o, (toExp (map fst ps)

137− (\ l s p -> Imp l s p False) t'))),

137+ (\ l s p -> Imp l s p Nothing) t'))),

138 (n, (syn, o, t) ) )

139 tdecl _ _ = ifail "Not allowed in a class declaration"

140

src/Idris/Elab/Clause.hs+1−1

@@ -867,7 +867,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

867 let wargval = getRetTy cwvalN

868 let wargtype = getRetTy cwvaltyN

869 logLvl 5 ("Abstract over " ++ show wargval ++ " in " ++ show wargtype)

870− let wtype = bindTyArgs (flip (Pi False) (TType (UVar 0))) (bargs_pre ++

870+ let wtype = bindTyArgs (flip (Pi Nothing) (TType (UVar 0))) (bargs_pre ++

871 (sMN 0 "warg", wargtype) :

872 map (abstract (sMN 0 "warg") wargval wargtype) bargs_post)

873 (substTerm wargval (P Bound (sMN 0 "warg") wargtype) ret_ty)

src/Idris/Elab/Type.hs+1−1

@@ -104,7 +104,7 @@ buildType info syn fc opts n ty' = do

104

105 return (cty, ckind, ty, inacc)

106 where

107− patToImp (Bind n (PVar t) sc) = Bind n (Pi False t (TType (UVar 0))) (patToImp sc)

107+ patToImp (Bind n (PVar t) sc) = Bind n (Pi Nothing t (TType (UVar 0))) (patToImp sc)

108 patToImp (Bind n b sc) = Bind n b (patToImp sc)

109 patToImp t = t

110

src/Idris/ElabDecls.hs+7−7

@@ -103,9 +103,9 @@ elabPrims = do mapM_ (elabDecl' EAll recinfo)

103

104 p_believeMe [_,_,x] = Just x

105 p_believeMe _ = Nothing

106− believeTy = Bind (sUN "a") (Pi False (TType (UVar (-2))) (TType (UVar (-1))))

106+ believeTy = Bind (sUN "a") (Pi Nothing (TType (UVar (-2))) (TType (UVar (-1))))

107− (Bind (sUN "b") (Pi False (TType (UVar (-2))) (TType (UVar (-1))))

107+ (Bind (sUN "b") (Pi Nothing (TType (UVar (-2))) (TType (UVar (-1))))

108− (Bind (sUN "x") (Pi False (V 1) (TType (UVar (-1)))) (V 1)))

108+ (Bind (sUN "x") (Pi Nothing (V 1) (TType (UVar (-1)))) (V 1)))

109 elabBelieveMe

110 = do let prim__believe_me = sUN "prim__believe_me"

111 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)

@@ -126,10 +126,10 @@ elabPrims = do mapM_ (elabDecl' EAll recinfo)

126 vnNothing = VP (DCon 0 1 False) (sNS (sUN "Nothing") ["Maybe", "Prelude"]) VErased

127 vnRefl = VP (DCon 0 2 False) eqCon VErased

128

129− synEqTy = Bind (sUN "a") (Pi False (TType (UVar (-3))) (TType (UVar (-2))))

129+ synEqTy = Bind (sUN "a") (Pi Nothing (TType (UVar (-3))) (TType (UVar (-2))))

130− (Bind (sUN "b") (Pi False (TType (UVar (-3))) (TType (UVar (-2))))

130+ (Bind (sUN "b") (Pi Nothing (TType (UVar (-3))) (TType (UVar (-2))))

131− (Bind (sUN "x") (Pi False (V 1) (TType (UVar (-2))))

131+ (Bind (sUN "x") (Pi Nothing (V 1) (TType (UVar (-2))))

132− (Bind (sUN "y") (Pi False (V 1) (TType (UVar (-2))))

132+ (Bind (sUN "y") (Pi Nothing (V 1) (TType (UVar (-2))))

133 (mkApp nMaybe [mkApp (P (TCon 0 4) eqTy Erased)

134 [V 3, V 2, V 1, V 0]]))))

135 elabSynEq

src/Idris/ElabTerm.hs+27−17

@@ -435,13 +435,20 @@ elab ist info emode opts fn tm

435 bindable (UN xs) = True

436 bindable n = implicitable n

437 elab' ina _ f@(PInferRef fc n) = elab' ina (Just fc) (PApp fc f [])

438− elab' ina _ tm@(PRef fc n)

438+ elab' ina fc' tm@(PRef fc n)

439 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)

440 && isTConName n (tt_ctxt ist)

441 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

442 | pattern && not reflection && e_nomatching ina

443 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

444+ | otherwise =

445+ do fty <- get_type (Var n) -- check for implicits

446+ ctxt <- get_context

447+ env <- get_env

448+ let a' = insertScopedImps fc (normalise ctxt env fty) []

449+ if null a'

444− | otherwise = erun fc $ do apply (Var n) []; solve

450+ then erun fc $ do apply (Var n) []; solve

451+ else elab' ina fc' (PApp fc tm [])

445 elab' ina _ (PLam fc n Placeholder sc)

452 elab' ina _ (PLam fc n Placeholder sc)

446 = do -- if n is a type constructor name, this makes no sense...

453 = do -- if n is a type constructor name, this makes no sense...

447 ctxt <- get_context

454 ctxt <- get_context

@@ -565,7 +572,7 @@ elab ist info emode opts fn tm

565 ans <- claimArgTys env xs

572 ans <- claimArgTys env xs

566 return ((aval, (True, (Var an))) : ans)

573 return ((aval, (True, (Var an))) : ans)

567 fnTy [] ret = forget ret

574 fnTy [] ret = forget ret

568− fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi False xt RType) (fnTy xs ret)

575+ fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi Nothing xt RType) (fnTy xs ret)

569

576

570 localVar env (PRef _ x)

577 localVar env (PRef _ x)

571 = case lookup x env of

578 = case lookup x env of

@@ -603,17 +610,17 @@ elab ist info emode opts fn tm

603 ty <- goal

610 ty <- goal

604 fty <- get_type (Var f)

611 fty <- get_type (Var f)

605 ctxt <- get_context

612 ctxt <- get_context

606− let args = insertScopedImps (normalise ctxt env fty) args_in

613+ let args = insertScopedImps fc (normalise ctxt env fty) args_in

607 let unmatchableArgs = if pattern

614 let unmatchableArgs = if pattern

608 then getUnmatchable (tt_ctxt ist) f

615 then getUnmatchable (tt_ctxt ist) f

609 else []

616 else []

610 -- Dot it if we're in a pattern and it isn't a constructor

617 -- Dot it if we're in a pattern and it isn't a constructor

611-- when (pattern && not (isDConName f ctxt) && f /= fn) $ dotterm

618-- when (pattern && not (isDConName f ctxt) && f /= fn) $ dotterm

612−

619+

613 when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)

620 when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)

614 && isTConName f (tt_ctxt ist)) $

621 && isTConName f (tt_ctxt ist)) $

615 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

622 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

616− if (f `elem` map fst env && length args == 1)

623+ if (f `elem` map fst env && length args == 1 && length args_in == 1)

617 then -- simple app, as below

624 then -- simple app, as below

618 do simple_app (elabE ina (Just fc) (PRef fc f))

625 do simple_app (elabE ina (Just fc) (PRef fc f))

619 (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))

626 (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))

@@ -1052,11 +1059,14 @@ elab ist info emode opts fn tm

1052 notImplicitable (PCase _ _ _) = True

1059 notImplicitable (PCase _ _ _) = True

1053 notImplicitable _ = False

1060 notImplicitable _ = False

1054

1061

1055− insertScopedImps (Bind n (Pi True _ _) sc) xs

1062+ insertScopedImps fc (Bind n (Pi im@(Just i) _ _) sc) xs

1063+ | tcinstance i

1064+ = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs

1065+ | otherwise

1056− = pimp n Placeholder True : insertScopedImps sc xs

1066+ = pimp n Placeholder True : insertScopedImps fc sc xs

1057− insertScopedImps (Bind n (Pi _ _ _) sc) (x : xs)

1067+ insertScopedImps fc (Bind n (Pi _ _ _) sc) (x : xs)

1058− = x : insertScopedImps sc xs

1068+ = x : insertScopedImps fc sc xs

1059− insertScopedImps _ xs = xs

1069+ insertScopedImps _ _ xs = xs

1060

1070

1061 insertImpLam t =

1071 insertImpLam t =

1062 do ty <- goal

1072 do ty <- goal

@@ -1064,10 +1074,10 @@ elab ist info emode opts fn tm

1064 let ty' = normalise (tt_ctxt ist) env ty

1074 let ty' = normalise (tt_ctxt ist) env ty

1065 addLam ty' t

1075 addLam ty' t

1066 where

1076 where

1077+ -- just one level at a time

1067− addLam (Bind n (Pi True _ _) sc) t

1078+ addLam (Bind n (Pi (Just _) _ _) sc) t

1068 = do impn <- unique_hole (sMN 0 "imp")

1079 = do impn <- unique_hole (sMN 0 "imp")

1069− t' <- addLam sc t

1070− return (PLam emptyFC impn Placeholder t')

1080+ return (PLam emptyFC impn Placeholder t)

1071 addLam _ t = return t

1081 addLam _ t = return t

1072

1082

1073 insertCoerce ina t@(PCase _ _ _) = return t

1083 insertCoerce ina t@(PCase _ _ _) = return t

@@ -1537,9 +1547,9 @@ runTac autoSolve ist perhapsFC fn tac

1537 where tacticTy = Var (reflm "Tactic")

1547 where tacticTy = Var (reflm "Tactic")

1538 listTy = Var (sNS (sUN "List") ["List", "Prelude"])

1548 listTy = Var (sNS (sUN "List") ["List", "Prelude"])

1539 scriptTy = (RBind (sMN 0 "__pi_arg")

1549 scriptTy = (RBind (sMN 0 "__pi_arg")

1540− (Pi False (RApp listTy envTupleType) RType)

1550+ (Pi Nothing (RApp listTy envTupleType) RType)

1541 (RBind (sMN 1 "__pi_arg")

1551 (RBind (sMN 1 "__pi_arg")

1542− (Pi False (Var $ reflm "TT") RType) tacticTy))

1552+ (Pi Nothing (Var $ reflm "TT") RType) tacticTy))

1543 runT (ByReflection tm) -- run the reflection function 'tm' on the

1553 runT (ByReflection tm) -- run the reflection function 'tm' on the

1544 -- goal, then apply the resulting reflected Tactic

1554 -- goal, then apply the resulting reflected Tactic

1545 = do tgoal <- goal

1555 = do tgoal <- goal

@@ -1812,7 +1822,7 @@ reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)

1812reifyTTBinderApp reif f [t]

1822reifyTTBinderApp reif f [t]

1813 | f == reflm "Lam" = liftM Lam (reif t)

1823 | f == reflm "Lam" = liftM Lam (reif t)

1814reifyTTBinderApp reif f [t, k]

1824reifyTTBinderApp reif f [t, k]

1815− | f == reflm "Pi" = liftM2 (Pi False) (reif t) (reif k)

1825+ | f == reflm "Pi" = liftM2 (Pi Nothing) (reif t) (reif k)

1816reifyTTBinderApp reif f [x, y]

1826reifyTTBinderApp reif f [x, y]

1817 | f == reflm "Let" = liftM2 Let (reif x) (reif y)

1827 | f == reflm "Let" = liftM2 Let (reif x) (reif y)

1818reifyTTBinderApp reif f [x, y]

1828reifyTTBinderApp reif f [x, y]

src/Idris/ParseExpr.hs+30−15

@@ -855,14 +855,18 @@ Pi' ::=

855@

856 -}

857

858+bindsymbol opts st syn

859+ = do symbol "->"

860+ return (Exp opts st False)

861+

858pi :: SyntaxInfo -> IdrisParser PTerm

862pi :: SyntaxInfo -> IdrisParser PTerm

859pi syn =

863pi syn =

860 do opts <- piOpts syn

864 do opts <- piOpts syn

861 st <- static

865 st <- static

862 (do xt <- try (lchar '(' *> typeDeclList syn <* lchar ')')

866 (do xt <- try (lchar '(' *> typeDeclList syn <* lchar ')')

863− symbol "->"

867+ binder <- bindsymbol opts st syn

864 sc <- expr syn

868 sc <- expr syn

865− return (bindList (PPi (Exp opts st False)) xt sc)) <|> (do

869+ return (bindList (PPi binder) xt sc)) <|> (do

866 (do try (lchar '{' *> reserved "auto")

870 (do try (lchar '{' *> reserved "auto")

867 when (st == Static) $ fail "auto type constraints can not be lazy or static"

871 when (st == Static) $ fail "auto type constraints can not be lazy or static"

868 xt <- typeDeclList syn

872 xt <- typeDeclList syn

@@ -881,12 +885,20 @@ pi syn =

881 return (bindList (PPi (TacImp [] Dynamic script)) xt sc))

885 return (bindList (PPi (TacImp [] Dynamic script)) xt sc))

882 <|> (do xt <- try (lchar '{' *> typeDeclList syn <* lchar '}')

886 <|> (do xt <- try (lchar '{' *> typeDeclList syn <* lchar '}')

883 symbol "->"

887 symbol "->"

888+ cs <- constraintList syn

884 sc <- expr syn

889 sc <- expr syn

890+ let (im,cl)

885− return (bindList (PPi (Imp opts st False (not (implicitAllowed syn)))) xt sc)))

891+ = if implicitAllowed syn

892+ then (Imp opts st False Nothing,

893+ constraint)

894+ else (Imp opts st False (Just (Impl False)),

895+ Imp opts st False (Just (Impl True)))

896+ return (bindList (PPi im) xt

897+ (bindList (PPi cl) cs sc))))

886 <|> (do x <- opExpr syn

898 <|> (do x <- opExpr syn

887− (do symbol "->"

899+ (do binder <- bindsymbol opts st syn

888 sc <- expr syn

900 sc <- expr syn

889− return (PPi (Exp opts st False) (sUN "__pi_arg") x sc))

901+ return (PPi binder (sUN "__pi_arg") x sc))

890 <|> return x)

902 <|> return x)

891 <?> "dependent type signature"

903 <?> "dependent type signature"

892

904

@@ -911,16 +923,19 @@ ConstraintList ::=

911@

923@

912-}

924-}

913constraintList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]

925constraintList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]

914−constraintList syn = try (do lchar '('

926+constraintList syn = try (constraintList1 syn)

927+ <|> return []

928+

929+constraintList1 :: SyntaxInfo -> IdrisParser [(Name, PTerm)]

930+constraintList1 syn = try (do lchar '('

915− tys <- sepBy1 nexpr (lchar ',')

931+ tys <- sepBy1 nexpr (lchar ',')

916− lchar ')'

932+ lchar ')'

917− reservedOp "=>"

933+ reservedOp "=>"

918− return tys)

934+ return tys)

919− <|> try (do t <- expr (disallowImp syn)

935+ <|> try (do t <- expr (disallowImp syn)

920− reservedOp "=>"

936+ reservedOp "=>"

921− return [(defname, t)])

937+ return [(defname, t)])

922− <|> return []

923− <?> "type constraint list"

938+ <?> "type constraint list"

924 where nexpr = try (do n <- name; lchar ':'

939 where nexpr = try (do n <- name; lchar ':'

925 e <- expr' (disallowImp syn)

940 e <- expr' (disallowImp syn)

926 return (n, e))

941 return (n, e))

src/Idris/Primitives.hs+1−1

@@ -26,7 +26,7 @@ data Prim = Prim { p_name :: Name,

26

27ty :: [Const] -> Const -> Type

28ty [] x = Constant x

29−ty (t:ts) x = Bind (sMN 0 "T") (Pi False (Constant t) (TType (UVar (-3)))) (ty ts x)

29+ty (t:ts) x = Bind (sMN 0 "T") (Pi Nothing (Constant t) (TType (UVar (-3)))) (ty ts x)

30

31total, partial, iopartial :: Totality

32total = Total []

src/Idris/TypeSearch.hs+1−1

@@ -416,7 +416,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

416 unifyQueue state [] = return state

417 unifyQueue state ((ty1, ty2) : queue) = do

418 --trace ("go: \n" ++ show state) True `seq` return ()

419− res <- tcToMaybe $ match_unify ctxt [ (n, Pi False ty (TType (UVar 0))) | (n, ty) <- holes state] ty1 ty2 [] (map fst $ holes state) []

419+ res <- tcToMaybe $ match_unify ctxt [ (n, Pi Nothing ty (TType (UVar 0))) | (n, ty) <- holes state] ty1 ty2 [] (map fst $ holes state) []

420 (state', queueAdditions) <- resolveUnis res state

421 guard $ scoreCriterion (score state')

422 unifyQueue state' (queue ++ queueAdditions)

test/basic012/basic012.idrnew file+62

@@ -0,0 +1,62 @@

1+import Data.Vect

2+import Control.Monad.State

3+import Control.Monad.Identity

4+

5+VThing : Type

6+VThing = {n : Nat} -> Vect n Int -> Int

7+

8+foo : Int -> Vect m Int -> ({n : Nat} -> Vect n Int -> Int) -> Int

9+foo x xs f = x + f xs

10+

11+foo' : Int -> Vect m Int -> VThing -> Int

12+foo' x xs f = x + f xs

13+

14+bar : Int -> VThing

15+bar y [] = 0

16+bar y (x :: xs) = y + x + bar y xs

17+

18+vsum : Vect n Int -> Int

19+vsum [] = 0

20+vsum (x :: xs) = x + vsum xs

21+

22+testfoo : Vect n Int -> Int

23+testfoo xs = foo 42 xs (\ xs => vsum xs)

24+

25+testfoo2 : Vect n Int -> Int

26+testfoo2 xs = foo' 42 xs vsum

27+

28+testfoo3 : Vect n Int -> Int

29+testfoo3 xs = foo 42 xs (bar 10)

30+

31+AnyST : Type -> Type -> Type

32+AnyST s a = {m : _} -> Monad m => StateT s m a

33+

34+foost: AnyST Int ()

35+foost = do x <- get

36+ put x

37+

38+wibble : StateT Int Maybe ()

39+wibble = foost

40+

41+appShow : Show a => ({b : _} -> Show b => b -> String) -> a -> String

42+appShow s x = s x

43+

44+myshow : Show a => a -> String

45+myshow = show

46+

47+baz : Int -> String

48+baz x = appShow myshow x ++ appShow show x

49+

50+tupleId : ({a : _} -> a -> a) -> (a, b) -> (a, b)

51+tupleId f (a, b) = (f a, f b)

52+

53+AppendType : Type

54+AppendType = {a, n, m : _} -> Vect n a -> Vect m a -> Vect (n + m) a

55+

56+append : AppendType

57+append [] ys = ys

58+append (x :: xs) ys = x :: append xs ys

59+

60+main : IO ()

61+main = do putStrLn (baz 42)

62+ print (append [1,2,3] [4,5,6])

test/basic012/expectednew file+2

@@ -0,0 +1,2 @@

1+4242

2+[1, 2, 3, 4, 5, 6]

test/basic012/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ basic012.idr -o basic012

3+./basic012

4+rm -f basic012 *.ibc

test/proof007/expected+1−1

@@ -1,3 +1,3 @@

1−DefaultArgUnknownName.idr:5:30:When elaborating right hand side of test:

1+DefaultArgUnknownName.idr:9:6:When elaborating right hand side of test:

2When elaborating argument [95marg[0m to function [92mDefaultArgUnknownName.funWithBadDefArg[0m:

3 No such variable sadgjhsag