c729d2f · Idris-dev · git.iko.soy

CHANGELOG+3

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

22--------------

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

44 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 : _}

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

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

710 the names exported from that module.

idris.cabal+3

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

321321 test/basic011/run

322322 test/basic011/*.idr

323323 test/basic011/expected

324+ test/basic012/run

325+ test/basic012/*.idr

326+ test/basic012/expected

324327

325328 test/buffer001-disabled/*.idr

326329 test/buffer001-disabled/run

src/Idris/AbsSyntax.hs+5−5

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

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

12431243 doAdd (UImplicit n ty : cs) ns t

12441244 | 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)

12461246 | otherwise = doAdd cs ns t

12471247

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

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

12501250 bindFree (n:ns) tm

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

12521252 | otherwise

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

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

12541254

12551255 getArgnames (PPi _ n c sc)

12561256 = n : getArgnames sc

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

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

12661266 collectImps _ = []

12671267

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

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

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

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

12711271 where

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

14271427 pibind using [] sc = sc

14281428 pibind using (n:ns) sc

14291429 = case lookup n using of

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

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

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

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

14321432 (pibind using ns sc)

14331433

14341434-- Add implicit arguments in function calls

src/Idris/AbsSyntaxTree.hs+7−6

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

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

490490 pstatic :: Static,

491491 pparam :: Bool,

492− pscoped :: Bool -- forall bound

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

493493 }

494494 | Exp { pargopts :: [ArgOpt],

495495 pstatic :: Static,

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

506506deriving instance NFData Plicity

507507!-}

508508

509−is_scoped :: Plicity -> Bool

509+is_scoped :: Plicity -> Maybe ImplicitInfo

510510is_scoped (Imp _ _ _ s) = s

511−is_scoped _ = False

511+is_scoped _ = Nothing

512512

513−impl = Imp [] Dynamic False False

514−forall_imp = Imp [] Dynamic False True

513+impl = Imp [] Dynamic False Nothing

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

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

515516expl = Exp [] Dynamic False

516517expl_param = Exp [] Dynamic True

517518constraint = Constraint [] Static

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

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

11481149

11491150getInferType (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))

11511152 toTy (PVar t) = PVTy t

11521153 toTy b = b

11531154getInferType (App (App _ ty) _) = ty

src/Idris/Core/Binary.hs+7

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

403403 return (RUType x1)

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

405405

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)

406413

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

408415 put x

src/Idris/Core/DeepSeq.hs+3

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

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

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

9191

92+instance NFData ImplicitInfo where

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

94+

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

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

9497 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)

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

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

371371

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

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

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

374374

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

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

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

661661 claim a RType

662662 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))

664664 movelast a

665665 movelast b

666666 fill (Var f)

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

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

676676 claim a RType

677677 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))

679679 tm <- get_term

680680 start_unify s

681681 claim s (Var a)

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

698698

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

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

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

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

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

703703 claim ty RType

704704 movelast ty

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

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

6969 | CheckIn Raw

7070 | Intro (Maybe Name)

7171 | IntroTy Raw (Maybe Name)

72− | Forall Name Bool Raw

72+ | Forall Name (Maybe ImplicitInfo) Raw

7373 | LetBind Name Raw Raw

7474 | ExpandLet Name Term

7575 | Rewrite Raw

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

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

413413 where

414414 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)

416416

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

418418

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

569569 _ -> lift $ tfail $ CantIntroduce t'

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

571571

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

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

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

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

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

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

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

672672deriving instance NFData Raw

673673!-}

674674

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+

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

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

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

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

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

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

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

682− | Pi { binderImpl :: Bool,

690+ | Pi { binderImpl :: Maybe ImplicitInfo,

683691 binderTy :: !b,

684692 binderKind :: !b }

685693 {-^ 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

230230 return (PVTy tv, tt')

231231

232232 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)

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

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

236236 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

5757 _ -> PRef un n

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

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

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

61− = PPi (Imp [] Dynamic False True) n (de env [] ty) (de ((n,n):env) is 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

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

6265 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)

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

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

6669 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

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

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

136136 (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'))),

138138 (n, (syn, o, t) ) )

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

140140

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

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

867867 let wargval = getRetTy cwvalN

868868 let wargtype = getRetTy cwvaltyN

869869 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 ++

871871 (sMN 0 "warg", wargtype) :

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

873873 (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

104104

105105 return (cty, ckind, ty, inacc)

106106 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)

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

109109 patToImp t = t

110110

src/Idris/ElabDecls.hs+7−7

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

103103

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

105105 p_believeMe _ = Nothing

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

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

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

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

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

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

109109 elabBelieveMe

110110 = do let prim__believe_me = sUN "prim__believe_me"

111111 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)

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

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

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

128128

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

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

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

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

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

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

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

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

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

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

135135 elabSynEq

src/Idris/ElabTerm.hs+27−17

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

435435 bindable (UN xs) = True

436436 bindable n = implicitable n

437437 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)

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

440440 && isTConName n (tt_ctxt ist)

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

442442 | pattern && not reflection && e_nomatching ina

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

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

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'

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

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

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

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

447454 ctxt <- get_context

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

565572 ans <- claimArgTys env xs

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

567574 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)

569576

570577 localVar env (PRef _ x)

571578 = case lookup x env of

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

603610 ty <- goal

604611 fty <- get_type (Var f)

605612 ctxt <- get_context

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

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

607614 let unmatchableArgs = if pattern

608615 then getUnmatchable (tt_ctxt ist) f

609616 else []

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

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

612−

619+

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

614621 && isTConName f (tt_ctxt ist)) $

615622 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)

617624 then -- simple app, as below

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

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

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

10521059 notImplicitable (PCase _ _ _) = True

10531060 notImplicitable _ = False

10541061

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

1056− = pimp n Placeholder True : insertScopedImps sc xs

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

1058− = x : insertScopedImps sc xs

1059− insertScopedImps _ xs = 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

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

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

1068+ = x : insertScopedImps fc sc xs

1069+ insertScopedImps _ _ xs = xs

10601070

10611071 insertImpLam t =

10621072 do ty <- goal

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

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

10651075 addLam ty' t

10661076 where

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

1077+ -- just one level at a time

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

10681079 = 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)

10711081 addLam _ t = return t

10721082

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

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

15371547 where tacticTy = Var (reflm "Tactic")

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

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

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

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

15411551 (RBind (sMN 1 "__pi_arg")

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

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

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

15441554 -- goal, then apply the resulting reflected Tactic

15451555 = do tgoal <- goal

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

18121822reifyTTBinderApp reif f [t]

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

18141824reifyTTBinderApp 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)

18161826reifyTTBinderApp reif f [x, y]

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

18181828reifyTTBinderApp reif f [x, y]

src/Idris/ParseExpr.hs+30−15

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

855855@

856856 -}

857857

858+bindsymbol opts st syn

859+ = do symbol "->"

860+ return (Exp opts st False)

861+

858862pi :: SyntaxInfo -> IdrisParser PTerm

859863pi syn =

860864 do opts <- piOpts syn

861865 st <- static

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

863− symbol "->"

867+ binder <- bindsymbol opts st syn

864868 sc <- expr syn

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

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

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

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

868872 xt <- typeDeclList syn

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

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

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

883887 symbol "->"

888+ cs <- constraintList syn

884889 sc <- expr syn

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

890+ let (im,cl)

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))))

886898 <|> (do x <- opExpr syn

887− (do symbol "->"

899+ (do binder <- bindsymbol opts st syn

888900 sc <- expr syn

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

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

890902 <|> return x)

891903 <?> "dependent type signature"

892904

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

911923@

912924-}

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

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

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

916− lchar ')'

917− reservedOp "=>"

918− return tys)

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

920− reservedOp "=>"

921− return [(defname, t)])

922− <|> return []

923− <?> "type constraint list"

926+constraintList syn = try (constraintList1 syn)

927+ <|> return []

928+

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

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

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

932+ lchar ')'

933+ reservedOp "=>"

934+ return tys)

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

936+ reservedOp "=>"

937+ return [(defname, t)])

938+ <?> "type constraint list"

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

925940 e <- expr' (disallowImp syn)

926941 return (n, e))

src/Idris/Primitives.hs+1−1

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

2626

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

2828ty [] 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)

3030

3131total, partial, iopartial :: Totality

3232total = Total []

src/Idris/TypeSearch.hs+1−1

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

416416 unifyQueue state [] = return state

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

418418 --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) []

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

421421 guard $ scoreCriterion (score state')

422422 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:

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

33 No such variable sadgjhsag