9ec3ec7 · 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+16−15

@@ -1124,10 +1124,10 @@ addStatics n tm ptm =

11241124 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }

11251125 addIBC (IBCStatic n)

11261126 where

1127− initStatics (Bind n (Pi ty _) sc) (PPi p n' t s)

1127+ initStatics (Bind n (Pi _ ty _) sc) (PPi p n' t s)

11281128 | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' t s) in

11291129 (static, (n, ty) : dynamic)

1130− initStatics (Bind n (Pi ty _) sc) (PPi p n' _ s)

1130+ initStatics (Bind n (Pi _ ty _) sc) (PPi p n' _ s)

11311131 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in

11321132 if pstatic p == Static then ((n, ty) : static, dynamic)

11331133 else if (not (searchArg p))

@@ -1143,16 +1143,16 @@ addStatics n tm ptm =

11431143 getNamePos i ps (P _ n _ : as)

11441144 | i `elem` ps = n : getNamePos (i + 1) ps as

11451145 getNamePos i ps (_ : as) = getNamePos (i + 1) ps as

1146− getParamNames ist (Bind t (Pi (P _ n _) _) sc)

1146+ getParamNames ist (Bind t (Pi _ (P _ n _) _) sc)

11471147 = n : getParamNames ist sc

11481148 getParamNames ist _ = []

11491149

1150− getNamesFrom i ps (Bind n (Pi _ _) sc)

1150+ getNamesFrom i ps (Bind n (Pi _ _ _) sc)

11511151 | i `elem` ps = n : getNamesFrom (i + 1) ps sc

11521152 | otherwise = getNamesFrom (i + 1) ps sc

11531153 getNamesFrom i ps sc = []

11541154

1155− freeArgNames (Bind n (Pi ty _) sc)

1155+ freeArgNames (Bind n (Pi _ ty _) sc)

11561156 = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here

11571157 freeArgNames tm = let (_, args) = unApply tm in

11581158 concatMap freeNames args

@@ -1164,7 +1164,7 @@ addStatics n tm ptm =

11641164 searchArg (TacImp _ _ _) = True

11651165 searchArg _ = False

11661166

1167− staticList sts (Bind n (Pi _ _) sc) = (n `elem` sts) : staticList sts sc

1167+ staticList sts (Bind n (Pi _ _ _) sc) = (n `elem` sts) : staticList sts sc

11681168 staticList _ _ = []

11691169

11701170-- Dealing with implicit arguments

@@ -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) 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) 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,10 +1265,11 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)

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

12661266 collectImps _ = []

12671267

1268− getImps (Bind n (Pi t _) sc) imps

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

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

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

12701271 where

1271− argInfo n (Imp opt _ _) t'

1272+ argInfo n (Imp opt _ _ _) t'

12721273 = (True, PImp (getPriority i t') True opt n t')

12731274 argInfo n (Exp opt _ _) t'

12741275 = (InaccessibleArg `elem` opt,

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

12791280 argInfo n (TacImp opt _ scr) t'

12801281 = (InaccessibleArg `elem` opt,

12811282 PTacImplicit 10 opt n scr t')

1282− getImps (Bind n (Pi t _) sc) imps = impBind n t : getImps sc imps

1283+ getImps (Bind n (Pi _ t _) sc) imps = impBind n t : getImps sc imps

12831284 where impBind n t = (True, PImp 1 True [] n Placeholder)

12841285 getImps sc tm = []

12851286

@@ -1358,7 +1359,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

13581359 = do (decls, ns) <- get

13591360 let isn = concatMap (namesIn uvars ist) (map getTm as)

13601361 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1361− imps top env (PPi (Imp l _ _) n ty sc)

1362+ imps top env (PPi (Imp l _ _ _) n ty sc)

13621363 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]

13631364 (decls , ns) <- get

13641365 put (PImp (getPriority ist ty) True l n Placeholder : decls,

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

14261427 pibind using [] sc = sc

14271428 pibind using (n:ns) sc

14281429 = case lookup n using of

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

1430− Nothing -> PPi (Imp [] Dynamic 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

14311432 (pibind using ns sc)

14321433

14331434-- Add implicit arguments in function calls

@@ -1711,7 +1712,7 @@ stripUnmatchable :: IState -> PTerm -> PTerm

17111712stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

17121713 su :: PTerm -> PTerm

17131714 su (PRef fc f)

1714− | (Bind n (Pi t _) sc :_) <- lookupTy f (tt_ctxt i)

1715+ | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)

17151716 = Placeholder

17161717 su (PApp fc f@(PRef _ fn) args)

17171718 | isDConName fn ctxt

src/Idris/AbsSyntaxTree.hs+12−4

@@ -488,7 +488,9 @@ deriving instance NFData Static

488488-- Mark bindings with their explicitness, and laziness

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

490490 pstatic :: Static,

491− pparam :: Bool }

491+ pparam :: Bool,

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

493+ }

492494 | Exp { pargopts :: [ArgOpt],

493495 pstatic :: Static,

494496 pparam :: Bool } -- this is a param (rather than index)

@@ -504,7 +506,13 @@ deriving instance Binary Plicity

504506deriving instance NFData Plicity

505507!-}

506508

507−impl = Imp [] Dynamic False

509+is_scoped :: Plicity -> Maybe ImplicitInfo

510+is_scoped (Imp _ _ _ s) = s

511+is_scoped _ = Nothing

512+

513+impl = Imp [] Dynamic False Nothing

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

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

508516expl = Exp [] Dynamic False

509517expl_param = Exp [] Dynamic True

510518constraint = Constraint [] Static

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

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

11411149

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

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

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

11441152 toTy (PVar t) = PVTy t

11451153 toTy b = b

11461154getInferType (App (App _ ty) _) = ty

@@ -1326,7 +1334,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

13261334 case s of

13271335 Static -> text "[static]" <> space

13281336 _ -> empty

1329− prettySe p bnd (PPi (Imp l s _) n ty sc)

1337+ prettySe p bnd (PPi (Imp l s _ fa) n ty sc)

13301338 | ppopt_impl ppo =

13311339 bracket p startPrec $

13321340 lbrace <> bindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>

src/Idris/Apropos.hs+1−1

@@ -66,7 +66,7 @@ instance Apropos Def where

6666

6767instance Apropos (Binder (TT Name)) where

6868 isApropos str (Lam ty) = str == T.pack "\\" || isApropos str ty

69− isApropos str (Pi ty _) = str == T.pack "->" || isApropos str ty

69+ isApropos str (Pi _ ty _) = str == T.pack "->" || isApropos str ty

7070 isApropos str (Let ty val) = str == T.pack "let" || isApropos str ty || isApropos str val

7171 isApropos str (NLet ty val) = str == T.pack "let" || isApropos str ty || isApropos str val

7272 isApropos str _ = False -- these shouldn't occur in defined libraries

src/Idris/CaseSplit.hs+1−1

@@ -183,7 +183,7 @@ argTys ist (PRef fc n)

183183 = case lookupTy n (tt_ctxt ist) of

184184 [ty] -> map (tyName . snd) (getArgTys ty) ++ repeat Nothing

185185 _ -> repeat Nothing

186− where tyName (Bind _ (Pi _ _) _) = Just (sUN "->")

186+ where tyName (Bind _ (Pi _ _ _) _) = Just (sUN "->")

187187 tyName t | (P _ n _, _) <- unApply t = Just n

188188 | otherwise = Nothing

189189argTys _ _ = repeat Nothing

src/Idris/Core/Binary.hs+13−4

@@ -403,15 +403,23 @@ 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

409416 = case x of

410417 Lam x1 -> do putWord8 0

411418 put x1

412− Pi x1 x2 -> do putWord8 1

413− put x1

414− put x2

419+ Pi x1 x2 x3 -> do putWord8 1

420+ put x1

421+ put x2

422+ put x3

415423 Let x1 x2 -> do putWord8 2

416424 put x1

417425 put x2

@@ -437,7 +445,8 @@ instance (Binary b) => Binary (Binder b) where

437445 return (Lam x1)

438446 1 -> do x1 <- get

439447 x2 <- get

440− return (Pi x1 x2)

448+ x3 <- get

449+ return (Pi x1 x2 x3)

441450 2 -> do x1 <- get

442451 x2 <- get

443452 return (Let x1 x2)

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

@@ -370,7 +370,7 @@ toPat reflect tc = map $ toPat' []

370370 toPat' [] (Constant x) | isTypeConst x = PTyPat

371371 | otherwise = PConst x

372372

373− toPat' [] (Bind n (Pi t _) sc)

373+ toPat' [] (Bind n (Pi _ t _) sc)

374374 | reflect && noOccurrence n sc

375375 = PReflected (sUN "->") [toPat' [] t, toPat' [] sc]

376376

src/Idris/Core/DeepSeq.hs+4−1

@@ -89,9 +89,12 @@ 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` ()

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

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

9598 rnf (Let x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

9699 rnf (NLet x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

97100 rnf (Hole x1) = rnf x1 `seq` ()

src/Idris/Core/Elaborate.hs+22−17

@@ -268,7 +268,7 @@ checkInjective (tm, l, r) = do ctxt <- get_context

268268 isInj ctxt (App f a) = isInj ctxt f

269269 isInj ctxt (Constant _) = True

270270 isInj ctxt (TType _) = True

271− isInj ctxt (Bind _ (Pi _ _) sc) = True

271+ isInj ctxt (Bind _ (Pi _ _ _) sc) = True

272272 isInj ctxt _ = False

273273

274274-- get instance argument names

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

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

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

371371

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

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

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

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

374374

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

376376letbind n t v = processTactic' (LetBind n t v)

@@ -493,7 +493,9 @@ prepare_apply fn imps =

493493 env <- get_env

494494 -- let claims = getArgs ty imps

495495 -- claims <- mkClaims (normalise ctxt env ty) imps []

496− claims <- mkClaims (finalise ty) imps [] (map fst env)

496+ claims <- mkClaims (finalise ty)

497+ (normalise ctxt env (finalise ty))

498+ imps [] (map fst env)

497499 ES (p, a) s prev <- get

498500 -- reverse the claims we made so that args go left to right

499501 let n = length (filter not imps)

@@ -502,11 +504,12 @@ prepare_apply fn imps =

502504 return $! claims

503505 where

504506 mkClaims :: Type -- ^ The type of the operation being applied

507+ -> Type -- ^ Normalised version if we need it

505508 -> [Bool] -- ^ Whether the arguments are implicit

506509 -> [(Name, Name)] -- ^ Accumulator for produced claims

507510 -> [Name] -- ^ Hypotheses

508511 -> Elab' aux [(Name, Name)] -- ^ The names of the arguments and their holes, resp.

509− mkClaims (Bind n' (Pi t_in _) sc) (i : is) claims hs =

512+ mkClaims (Bind n' (Pi _ t_in _) sc) (Bind _ _ scn) (i : is) claims hs =

510513 do let t = rebind hs t_in

511514 n <- getNameFrom (mkMN n')

512515-- when (null claims) (start_unify n)

@@ -514,9 +517,11 @@ prepare_apply fn imps =

514517-- trace ("CLAIMING " ++ show (n, t) ++ " with " ++ show (fn, hs)) $

515518 claim n (forget t)

516519 when i (movelast n)

517− mkClaims sc' is ((n', n) : claims) hs

518− mkClaims t [] claims _ = return $! (reverse claims)

519− mkClaims _ _ _ _

520+ mkClaims sc' scn is ((n', n) : claims) hs

521+ -- if we run out of arguments, we need the normalised version...

522+ mkClaims t tn@(Bind _ _ sc) (i : is) cs hs = mkClaims tn tn (i : is) cs hs

523+ mkClaims t _ [] claims _ = return $! (reverse claims)

524+ mkClaims _ _ _ _ _

520525 | Var n <- fn

521526 = do ctxt <- get_context

522527 case lookupTy n ctxt of

@@ -614,7 +619,7 @@ apply_elab n args =

614619 priOrder _ Nothing = GT

615620 priOrder (Just (x, _)) (Just (y, _)) = compare x y

616621

617− doClaims (Bind n' (Pi t _) sc) (i : is) claims =

622+ doClaims (Bind n' (Pi _ t _) sc) (i : is) claims =

618623 do n <- unique_hole (mkMN n')

619624 when (null claims) (start_unify n)

620625 let sc' = instantiate (P Bound n t) sc

@@ -649,13 +654,13 @@ checkPiGoal :: Name -> Elab' aux ()

649654checkPiGoal n

650655 = do g <- goal

651656 case g of

652− Bind _ (Pi _ _) _ -> return ()

657+ Bind _ (Pi _ _ _) _ -> return ()

653658 _ -> do a <- getNameFrom (sMN 0 "pargTy")

654659 b <- getNameFrom (sMN 0 "pretTy")

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

656661 claim a RType

657662 claim b RType

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

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

659664 movelast a

660665 movelast b

661666 fill (Var f)

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

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

671676 claim a RType

672677 claim b RType

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

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

674679 tm <- get_term

675680 start_unify s

676681 claim s (Var a)

@@ -693,11 +698,11 @@ simple_app fun arg appstr =

693698

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

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

696−arg :: Name -> Name -> Elab' aux ()

697−arg n tyhole = do ty <- unique_hole tyhole

698− claim ty RType

699− movelast ty

700− forall n (Var ty)

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

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

703+ claim ty RType

704+ movelast ty

705+ forall n i (Var ty)

701706

702707-- try a tactic, if it adds any unification problem, return an error

703708no_errors :: Elab' aux () -> Maybe Err -> Elab' aux ()

src/Idris/Core/Evaluate.hs+2−2

@@ -459,7 +459,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

459459 | Just v <- findDefault alts = return $ Just (amap, v)

460460 chooseAlt env _ (VP _ n _, args) alts amap

461461 | Just (ns, sc) <- findFn n alts = return $ Just (updateAmap (zip ns args) amap, sc)

462− chooseAlt env _ (VBind _ _ (Pi s k) t, []) alts amap

462+ chooseAlt env _ (VBind _ _ (Pi i s k) t, []) alts amap

463463 | Just (ns, sc) <- findFn (sUN "->") alts

464464 = do t' <- t (VV 0) -- we know it's not in scope or it's not a pattern

465465 return $ Just (updateAmap (zip ns [s, t']) amap, sc)

@@ -602,7 +602,7 @@ convEq ctxt holes topx topy = ceq [] topx topy where

602602 where

603603 ceqB ps (Let v t) (Let v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

604604 ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

605− ceqB ps (Pi v t) (Pi v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

605+ ceqB ps (Pi i v t) (Pi i' v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

606606 ceqB ps b b' = ceq ps (binderTy b) (binderTy b')

607607 ceq ps (App fx ax) (App fy ay) = liftM2 (&&) (ceq ps fx fy) (ceq ps ax ay)

608608 ceq ps (Constant x) (Constant y) = return (x == y)

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

@@ -88,7 +88,7 @@ toTT (EBind n b body) = do n' <- newN n

8888 b' <- fixBinder b

8989 Bind n' b' <$> toTT body'

9090 where fixBinder (Lam t) = Lam <$> toTT t

91− fixBinder (Pi t k) = Pi <$> toTT t <*> toTT k

91+ fixBinder (Pi i t k) = Pi i <$> toTT t <*> toTT k

9292 fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2

9393 fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2

9494 fixBinder (Hole t) = Hole <$> toTT t

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

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

6969 | CheckIn Raw

7070 | Intro (Maybe Name)

7171 | IntroTy Raw (Maybe Name)

72− | Forall Name 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 (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

@@ -540,17 +540,17 @@ introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

540540 Just name -> name

541541 Nothing -> x

542542 let t' = case t of

543− x@(Bind y (Pi s _) _) -> x

543+ x@(Bind y (Pi _ s _) _) -> x

544544 _ -> hnf ctxt env t

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

546546-- ns <- lift $ unify ctxt env tyv t'

547547 case t' of

548− Bind y (Pi s _) t -> let t' = subst y (P Bound n s) t in

549− do ns <- unify' ctxt env s tyv

550− ps <- get

551− let (uh, uns) = unified ps

552−-- put (ps { unified = (uh, uns ++ ns) })

553− return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))

548+ Bind y (Pi _ s _) t -> let t' = subst y (P Bound n s) t in

549+ do ns <- unify' ctxt env s tyv

550+ ps <- get

551+ let (uh, uns) = unified ps

552+-- put (ps { unified = (uh, uns ++ ns) })

553+ return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))

554554 _ -> lift $ tfail $ CantIntroduce t'

555555introTy ty n ctxt env _ = fail "Can't introduce here."

556556

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

560560 Just name -> name

561561 Nothing -> x

562562 let t' = case t of

563− x@(Bind y (Pi s _) _) -> x

563+ x@(Bind y (Pi _ s _) _) -> x

564564 _ -> hnf ctxt env t

565565 case t' of

566− Bind y (Pi s _) t -> -- trace ("in type " ++ show t') $

566+ Bind y (Pi _ s _) t -> -- trace ("in type " ++ show t') $

567567 let t' = subst y (P Bound n s) t in

568568 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))

569569 _ -> lift $ tfail $ CantIntroduce t'

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

571571

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

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

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

573+forall 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))

576576 unify' ctxt env t (TType (UVar 0))

577− return $ Bind n (Pi tyv (TType (UVar 0))) (Bind x (Hole t) (P Bound x t))

578−forall n ty ctxt env _ = fail "Can't pi bind here"

577+ return $ Bind n (Pi impl tyv (TType (UVar 0))) (Bind x (Hole t) (P Bound x t))

578+forall n impl ty ctxt env _ = fail "Can't pi bind here"

579579

580580patvar :: Name -> RunTactic

581581patvar n ctxt env (Bind x (Hole t) sc) =

@@ -973,7 +973,7 @@ process t h = tactic (Just h) (mktac t)

973973 mktac HNF_Compute = hnf_compute

974974 mktac (Intro n) = intro n

975975 mktac (IntroTy ty n) = introTy ty n

976− mktac (Forall n t) = forall n t

976+ mktac (Forall n i t) = forall n i t

977977 mktac (LetBind n t v) = letbind n t v

978978 mktac (ExpandLet n b) = expandLet n b

979979 mktac (Rewrite t) = rewrite t

src/Idris/Core/TT.hs+29−17

@@ -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,9 +687,13 @@ 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 { binderTy :: !b,

690+ | Pi { binderImpl :: Maybe ImplicitInfo,

691+ binderTy :: !b,

683692 binderKind :: !b }

684− {-^ 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) -> ...@

694+ The 'binderImpl' flag says whether it was a scoped implicit

695+ (i.e. forall bound) in the high level Idris, but otherwise

696+ has no relevance in TT. -}

685697 | Let { binderTy :: !b,

686698 binderVal :: b {-^ value for bound variable-}}

687699 -- ^ A binding that occurs in a @let@ expression

@@ -703,7 +715,7 @@ deriving instance NFData Binder

703715

704716instance Sized a => Sized (Binder a) where

705717 size (Lam ty) = 1 + size ty

706− size (Pi ty _) = 1 + size ty

718+ size (Pi _ ty _) = 1 + size ty

707719 size (Let ty val) = 1 + size ty + size val

708720 size (NLet ty val) = 1 + size ty + size val

709721 size (Hole ty) = 1 + size ty

@@ -717,7 +729,7 @@ fmapMB f (Let t v) = liftM2 Let (f t) (f v)

717729fmapMB f (NLet t v) = liftM2 NLet (f t) (f v)

718730fmapMB f (Guess t v) = liftM2 Guess (f t) (f v)

719731fmapMB f (Lam t) = liftM Lam (f t)

720−fmapMB f (Pi t k) = liftM2 Pi (f t) (f k)

732+fmapMB f (Pi i t k) = liftM2 (Pi i) (f t) (f k)

721733fmapMB f (Hole t) = liftM Hole (f t)

722734fmapMB f (GHole i t) = liftM (GHole i) (f t)

723735fmapMB f (PVar t) = liftM PVar (f t)

@@ -884,7 +896,7 @@ isInjective (P (DCon _ _ _) _ _) = True

884896isInjective (P (TCon _ _) _ _) = True

885897isInjective (Constant _) = True

886898isInjective (TType x) = True

887−isInjective (Bind _ (Pi _ _) sc) = True

899+isInjective (Bind _ (Pi _ _ _) sc) = True

888900isInjective (App f a) = isInjective f

889901isInjective _ = False

890902

@@ -1099,7 +1111,7 @@ freeNames t = nub $ freeNames' t

10991111

11001112-- | Return the arity of a (normalised) type

11011113arity :: TT n -> Int

1102−arity (Bind n (Pi t _) sc) = 1 + arity sc

1114+arity (Bind n (Pi _ t _) sc) = 1 + arity sc

11031115arity _ = 0

11041116

11051117-- | Deconstruct an application; returns the function and a list of arguments

@@ -1159,13 +1171,13 @@ bindTyArgs b xs = bindAll (map (\ (n, ty) -> (n, b ty)) xs)

11591171getArgTys :: TT n -> [(n, TT n)]

11601172getArgTys (Bind n (PVar _) sc) = getArgTys sc

11611173getArgTys (Bind n (PVTy _) sc) = getArgTys sc

1162−getArgTys (Bind n (Pi t _) sc) = (n, t) : getArgTys sc

1174+getArgTys (Bind n (Pi _ t _) sc) = (n, t) : getArgTys sc

11631175getArgTys _ = []

11641176

11651177getRetTy :: TT n -> TT n

11661178getRetTy (Bind n (PVar _) sc) = getRetTy sc

11671179getRetTy (Bind n (PVTy _) sc) = getRetTy sc

1168−getRetTy (Bind n (Pi _ _) sc) = getRetTy sc

1180+getRetTy (Bind n (Pi _ _ _) sc) = getRetTy sc

11691181getRetTy sc = sc

11701182

11711183uniqueNameFrom :: [Name] -> [Name] -> Name

@@ -1281,7 +1293,7 @@ prettyEnv env t = prettyEnv' env t False

12811293 else

12821294 lbracket <+> text (show i) <+> rbracket

12831295 | otherwise = text "unbound" <+> text (show i) <+> text "!"

1284− prettySe p env (Bind n b@(Pi t _) sc) debug

1296+ prettySe p env (Bind n b@(Pi _ t _) sc) debug

12851297 | noOccurrence n sc && not debug =

12861298 bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug

12871299 prettySe p env (Bind n b sc) debug =

@@ -1297,7 +1309,7 @@ prettyEnv env t = prettyEnv' env t False

12971309 -- Render a `Binder` and its name

12981310 prettySb env n (Lam t) = prettyB env "λ" "=>" n t

12991311 prettySb env n (Hole t) = prettyB env "?defer" "." n t

1300− prettySb env n (Pi t _) = prettyB env "(" ") ->" n t

1312+ prettySb env n (Pi _ t _) = prettyB env "(" ") ->" n t

13011313 prettySb env n (PVar t) = prettyB env "pat" "." n t

13021314 prettySb env n (PVTy t) = prettyB env "pty" "." n t

13031315 prettySb env n (Let t v) = prettyBv env "let" "in" n t v

@@ -1323,7 +1335,7 @@ showEnv' env t dbg = se 10 env t where

13231335 = (show $ fst $ env!!i) ++

13241336 if dbg then "{" ++ show i ++ "}" else ""

13251337 | otherwise = "!!V " ++ show i ++ "!!"

1326− se p env (Bind n b@(Pi t k) sc)

1338+ se p env (Bind n b@(Pi _ t k) sc)

13271339 | noOccurrence n sc && not dbg = bracket p 2 $ se 1 env t ++ arrow k ++ se 10 ((n,b):env) sc

13281340 where arrow (TType _) = " -> "

13291341 arrow u = " [" ++ show u ++ "] -> "

@@ -1339,7 +1351,7 @@ showEnv' env t dbg = se 10 env t where

13391351 sb env n (Lam t) = showb env "\\ " " => " n t

13401352 sb env n (Hole t) = showb env "? " ". " n t

13411353 sb env n (GHole i t) = showb env "?defer " ". " n t

1342− sb env n (Pi t _) = showb env "(" ") -> " n t

1354+ sb env n (Pi _ t _) = showb env "(" ") -> " n t

13431355 sb env n (PVar t) = showb env "pat " ". " n t

13441356 sb env n (PVTy t) = showb env "pty " ". " n t

13451357 sb env n (Let t v) = showbv env "let " " in " n t v

@@ -1399,7 +1411,7 @@ orderPats tm = op [] tm

13991411

14001412 op ps (Bind n (PVar t) sc) = op ((n, PVar t) : ps) sc

14011413 op ps (Bind n (Hole t) sc) = op ((n, Hole t) : ps) sc

1402− op ps (Bind n (Pi t k) sc) = op ((n, Pi t k) : ps) sc

1414+ op ps (Bind n (Pi i t k) sc) = op ((n, Pi i t k) : ps) sc

14031415 op ps sc = bindAll (sortP ps) sc

14041416

14051417 sortP ps = pick [] (reverse ps)

@@ -1445,10 +1457,10 @@ liftPats tm = let (tm', ps) = runState (getPats tm) [] in

14451457 v' <- getPats v

14461458 sc' <- getPats sc

14471459 return (Bind n (Let t' v') sc')

1448− getPats (Bind n (Pi t k) sc) = do t' <- getPats t

1449− k' <- getPats k

1450− sc' <- getPats sc

1451− return (Bind n (Pi t' k') sc')

1460+ getPats (Bind n (Pi i t k) sc) = do t' <- getPats t

1461+ k' <- getPats k

1462+ sc' <- getPats sc

1463+ return (Bind n (Pi i t' k') sc')

14521464 getPats (Bind n (Lam t) sc) = do t' <- getPats t

14531465 sc' <- getPats sc

14541466 return (Bind n (Lam t') sc')

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

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

8787 = do (fv, fty) <- chk u env f

8888 (av, aty) <- chk u env a

8989 let fty' = case uniqueBinders (map fst env) (finalise fty) of

90− ty@(Bind x (Pi s k) t) -> ty

90+ ty@(Bind x (Pi i s k) t) -> ty

9191 _ -> uniqueBinders (map fst env)

9292 $ case hnf ctxt env fty of

93− ty@(Bind x (Pi s k) t) -> ty

93+ ty@(Bind x (Pi i s k) t) -> ty

9494 _ -> normalise ctxt env fty

9595 case fty' of

96− Bind x (Pi s k) t ->

96+ Bind x (Pi i s k) t ->

9797 do convertsC ctxt env aty s

9898 let apty = simplify initContext env

9999 (Bind x (Let aty av) t)

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

133133 constType _ = TType (UVal 0)

134134 chk u env (RForce t) = do (_, ty) <- chk u env t

135135 return (Erased, ty)

136− chk u env (RBind n (Pi s k) t)

136+ chk u env (RBind n (Pi i s k) t)

137137 = do (sv, st) <- chk u env s

138138 (kv, kt) <- chk u env k

139− (tv, tt) <- chk st ((n, Pi sv kv) : env) t

139+ (tv, tt) <- chk st ((n, Pi i sv kv) : env) t

140140 (v, cs) <- get

141141 case (normalise ctxt env st, normalise ctxt env tt) of

142142 (TType su, TType tu) -> do

143143 when (not holes) $ put (v+1, ULE su (UVar v):ULE tu (UVar v):cs)

144144 let k' = st `smaller` kv `smaller` TType (UVar v) `smaller` u

145− return (Bind n (Pi (uniqueBinders (map fst env) sv) k')

145+ return (Bind n (Pi i (uniqueBinders (map fst env) sv) k')

146146 (pToV n tv), k')

147147 (un, un') ->

148148 let k' = st `smaller` kv `smaller` un `smaller` un' `smaller` u in

149− return (Bind n (Pi (uniqueBinders (map fst env) sv) k')

149+ return (Bind n (Pi i (uniqueBinders (map fst env) sv) k')

150150 (pToV n tv), k')

151151

152− where mkUniquePi kv (Bind n (Pi s k) sc)

152+ where mkUniquePi kv (Bind n (Pi i s k) sc)

153153 = let k' = smaller kv k in

154− Bind n (Pi s k') (mkUniquePi k' sc)

154+ Bind n (Pi i s k') (mkUniquePi k' sc)

155155 mkUniquePi kv (Bind n (Lam t) sc)

156156 = Bind n (Lam (mkUniquePi kv t)) (mkUniquePi kv sc)

157157 mkUniquePi kv (Bind n (Let t v) sc)

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

161161 -- Kind of the whole thing is the kind of the most unique thing

162162 -- in the environment (because uniqueness taints everything...)

163163 mostUnique [] k = k

164− mostUnique (Pi _ pk : es) k = mostUnique es (smaller pk k)

164+ mostUnique (Pi _ _ pk : es) k = mostUnique es (smaller pk k)

165165 mostUnique (_ : es) k = mostUnique es k

166166

167167 chk u env (RBind n b sc)

@@ -230,9 +230,9 @@ 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 t bt) sct)

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

235− = return (Bind n (Pi t k) scv, 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)

236236 discharge n (Let t v) bt scv sct

237237 = return (Bind n (Let t v) scv, Bind n (Let t v) sct)

238238 discharge n (NLet t v) bt scv sct

src/Idris/Core/Unify.hs+25−15

@@ -86,20 +86,30 @@ match_unify ctxt env topx topy inj holes from =

8686 return (map (renameBinders env) v')

8787 _ -> tfail e

8888 where

89− -- This rule is highly dubious... it certainly produces a valid answer

90− -- but it scares me. However, matching is never guaranteed to give a unique

91− -- answer, merely a valid one, so perhaps we're okay.

92− -- In other words: it may vanish without warning some day :)

9389 un :: [((Name, Name), TT Name)] -> TT Name -> TT Name ->

9490 StateT UInfo

9591 TC [(Name, TT Name)]

9692

97− un names x tm@(App (P _ f (Bind fn (Pi t _) sc)) a)

93+ -- This rule is highly dubious... it certainly produces a valid answer

94+ -- but it scares me. However, matching is never guaranteed to give a unique

95+ -- answer, merely a valid one, so perhaps we're okay.

96+ -- In other words: it may vanish without warning some day :)

97+ un names x tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a)

98+ | (P (TCon _ _) _ _, _) <- unApply x,

99+ holeIn env f || f `elem` holes

100+ = let n' = uniqueName (sMN 0 "mv") (map fst env) in

101+ checkCycle names (f, Bind n' (Lam t) x)

102+ un names tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a) x

103+ | (P (TCon _ _) _ _, _) <- unApply x,

104+ holeIn env f || f `elem` holes

105+ = let n' = uniqueName fn (map fst env) in

106+ checkCycle names (f, Bind n' (Lam t) x)

107+ un names x tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a)

98108 | (P (DCon _ _ _) _ _, _) <- unApply x,

99109 holeIn env f || f `elem` holes

100110 = let n' = uniqueName (sMN 0 "mv") (map fst env) in

101111 checkCycle names (f, Bind n' (Lam t) x)

102− un names tm@(App (P _ f (Bind fn (Pi t _) sc)) a) x

112+ un names tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a) x

103113 | (P (DCon _ _ _) _ _, _) <- unApply x,

104114 holeIn env f || f `elem` holes

105115 = let n' = uniqueName fn (map fst env) in

@@ -143,7 +153,7 @@ match_unify ctxt env topx topy inj holes from =

143153 h2 <- un bnames vx vy

144154 combine bnames h1 h2

145155 uB bnames (Lam tx) (Lam ty) = un bnames tx ty

146− uB bnames (Pi tx _) (Pi ty _) = un bnames tx ty

156+ uB bnames (Pi _ tx _) (Pi _ ty _) = un bnames tx ty

147157 uB bnames x y = do UI s f <- get

148158 let r = recoverable (normalise ctxt env (binderTy x))

149159 (normalise ctxt env (binderTy y))

@@ -431,18 +441,18 @@ unify ctxt env topx topy inj holes usersupp from =

431441 -- f D unifies with t -> D. This is dubious, but it helps with type

432442 -- class resolution for type classes over functions.

433443

434− un' fn bnames (App f x) (Bind n (Pi t k) y)

444+ un' fn bnames (App f x) (Bind n (Pi i t k) y)

435445 | noOccurrence n y && injectiveApp f

436446 = do ux <- un' False bnames x y

437447 uf <- un' False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

438− (Bind n (Pi t k) (V 1)))

448+ (Bind n (Pi i t k) (V 1)))

439449 combine bnames ux uf

440450

441− un' fn bnames (Bind n (Pi t k) y) (App f x)

451+ un' fn bnames (Bind n (Pi i t k) y) (App f x)

442452 | noOccurrence n y && injectiveApp f

443453 = do ux <- un' False bnames y x

444454 uf <- un' False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

445− (Bind n (Pi t k) (V 1))) f

455+ (Bind n (Pi i t k) (V 1))) f

446456 combine bnames ux uf

447457

448458 un' fn bnames (Bind x bx sx) (Bind y by sy)

@@ -451,7 +461,7 @@ unify ctxt env topx topy inj holes usersupp from =

451461 h2 <- un' False (((x,y),binderTy bx):bnames) sx sy

452462 combine bnames h1 h2

453463 where sameBinder (Lam _) (Lam _) = True

454− sameBinder (Pi _ _) (Pi _ _) = True

464+ sameBinder (Pi _ _ _) (Pi _ _ _) = True

455465 sameBinder _ _ = False

456466 un' fn bnames x y

457467 | OK True <- convEq' ctxt holes x y = do sc 1; return []

@@ -583,7 +593,7 @@ unify ctxt env topx topy inj holes usersupp from =

583593 sc 1

584594 combine bnames h1 h2

585595 uB bnames (Lam tx) (Lam ty) = do sc 1; un' False bnames tx ty

586− uB bnames (Pi tx _) (Pi ty _) = do sc 1; un' False bnames tx ty

596+ uB bnames (Pi _ tx _) (Pi _ ty _) = do sc 1; un' False bnames tx ty

587597 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty

588598 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty

589599 uB bnames x y = do UI s f <- get

@@ -686,10 +696,10 @@ recoverable (App f a) (App f' a')

686696 | f == f' = recoverable a a'

687697recoverable (App f a) (App f' a')

688698 = recoverable f f' -- && recoverable a a'

689−recoverable f (Bind _ (Pi _ _) sc)

699+recoverable f (Bind _ (Pi _ _ _) sc)

690700 | (P (DCon _ _ _) _ _, _) <- unApply f = False

691701 | (P (TCon _ _) _ _, _) <- unApply f = False

692−recoverable (Bind _ (Pi _ _) sc) f

702+recoverable (Bind _ (Pi _ _ _) sc) f

693703 | (P (DCon _ _ _) _ _, _) <- unApply f = False

694704 | (P (TCon _ _) _ _, _) <- unApply f = False

695705recoverable (Bind _ (Lam _) sc) f = recoverable sc f

src/Idris/Coverage.hs+4−4

@@ -286,12 +286,12 @@ checkPositive mut_ns (cn, ty')

286286 where

287287 args t = [0..length (getArgTys t)-1]

288288

289− cp (Bind n (Pi aty _) sc) = posArg aty && cp sc

289+ cp (Bind n (Pi _ aty _) sc) = posArg aty && cp sc

290290 cp t | (P _ n' _, args) <- unApply t,

291291 n' `elem` mut_ns = all noRec args

292292 cp _ = True

293293

294− posArg (Bind _ (Pi nty _) sc)

294+ posArg (Bind _ (Pi _ nty _) sc)

295295 | (P _ n' _, args) <- unApply nty

296296 = n' `notElem` mut_ns && all noRec args && posArg sc

297297 posArg t | (P _ n' _, args) <- unApply t,

@@ -536,8 +536,8 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

536536 = case lookupTy n (tt_ctxt ist) of

537537 [ty] -> expand 0 (normalise (tt_ctxt ist) [] ty) args

538538 _ -> args

539− where expand i (Bind n (Pi _ _) sc) (x : xs) = x : expand (i + 1) sc xs

540− expand i (Bind n (Pi _ _) sc) [] = Just (i, Same) : expand (i + 1) sc []

539+ where expand i (Bind n (Pi _ _ _) sc) (x : xs) = x : expand (i + 1) sc xs

540+ expand i (Bind n (Pi _ _ _) sc) [] = Just (i, Same) : expand (i + 1) sc []

541541 expand i _ xs = xs

542542

543543 mkChange n args pargs = [(n, expandToArity n (sizes args))]

src/Idris/DeepSeq.hs+2−2

@@ -94,8 +94,8 @@ instance NFData ArgOpt where

9494 rnf _ = ()

9595

9696instance NFData Plicity where

97− rnf (Imp x1 x2 x3)

98− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

97+ rnf (Imp x1 x2 x3 x4)

98+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

9999 rnf (Exp x1 x2 x3)

100100 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

101101 rnf (Constraint x1 x2)

src/Idris/Delaborate.hs+13−8

@@ -57,18 +57,23 @@ 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 ((PImp { argopts = opts }):is) (Bind n (Pi ty _) sc)

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

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

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

61+ | tcinstance impl

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

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

63+ | otherwise

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

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

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

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

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

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

6570 = PPi (tacimpl tac) n (de env [] ty) (de ((n,n):env) is sc)

66− de env (plic:is) (Bind n (Pi ty _) sc)

71+ de env (plic:is) (Bind n (Pi _ ty _) sc)

6772 = PPi (Exp (argopts plic) Dynamic False)

6873 n

6974 (de env [] ty)

7075 (de ((n,n):env) is sc)

71− de env [] (Bind n (Pi ty _) sc)

76+ de env [] (Bind n (Pi _ ty _) sc)

7277 = PPi expl n (de env [] ty) (de ((n,n):env) [] sc)

7378

7479 de env imps (Bind n (Let ty val) sc)

@@ -222,9 +227,9 @@ pprintErr' i (CantConvert x_in y_in env) =

222227 indented (annTm y_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)

223228 y)) <>

224229 if (opt_errContext (idris_options i)) then line <> showSc i env else empty

225− where flagUnique (Bind n (Pi t k@(UType u)) sc)

230+ where flagUnique (Bind n (Pi i t k@(UType u)) sc)

226231 = App (P Ref (sUN (show u)) Erased)

227− (Bind n (Pi (flagUnique t) k) (flagUnique sc))

232+ (Bind n (Pi i (flagUnique t) k) (flagUnique sc))

228233 flagUnique (App f a) = App (flagUnique f) (flagUnique a)

229234 flagUnique (Bind n b sc) = Bind n (fmap flagUnique b) (flagUnique sc)

230235 flagUnique t = t

src/Idris/Elab/Class.hs+5−4

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

133133 = do t' <- implicit' info syn allmeths n t

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

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

136− (n, (doc, o, (toExp (map fst ps) Imp t'))),

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

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

137138 (n, (syn, o, t) ) )

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

139140

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

200201 return [PTy doc [] syn fc o m ty',

201202 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

202203

203− getMArgs (PPi (Imp _ _ _) n ty sc) = IA : getMArgs sc

204+ getMArgs (PPi (Imp _ _ _ _) n ty sc) = IA : getMArgs sc

204205 getMArgs (PPi (Exp _ _ _) n ty sc) = EA : getMArgs sc

205206 getMArgs (PPi (Constraint _ _) n ty sc) = CA : getMArgs sc

206207 getMArgs _ = []

@@ -218,13 +219,13 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

218219 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns

219220 rhsArgs [] _ = []

220221

221− insertConstraint c (PPi p@(Imp _ _ _) n ty sc)

222+ insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)

222223 = PPi p n ty (insertConstraint c sc)

223224 insertConstraint c sc = PPi (constraint { pstatic = Static })

224225 (sMN 0 "class") c sc

225226

226227 -- make arguments explicit and don't bind class parameters

227− toExp ns e (PPi (Imp l s p) n ty sc)

228+ toExp ns e (PPi (Imp l s p _) n ty sc)

228229 | n `elem` ns = toExp ns e sc

229230 | otherwise = PPi (e l s p) n ty (toExp ns e sc)

230231 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)

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

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

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

923923 (crhs, crhsty) <- recheckC fc [] rhs'

924924 return $ (Right (clhs, crhs), lhs)

925925 where

926− getImps (Bind n (Pi _ _) t) = pexp Placeholder : getImps t

926+ getImps (Bind n (Pi _ _ _) t) = pexp Placeholder : getImps t

927927 getImps _ = []

928928

929929 mkAuxC wname lhs ns ns' (PClauses fc o n cs)

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

@@ -177,7 +177,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

177177 getDataApp f@(App _ _)

178178 | (P _ d _, args) <- unApply f

179179 = if (d == n) then [mParam args args] else []

180− getDataApp (Bind n (Pi t _) sc)

180+ getDataApp (Bind n (Pi _ t _) sc)

181181 = getDataApp t ++ getDataApp (instantiate (P Bound n t) sc)

182182 getDataApp _ = []

183183

src/Idris/Elab/Instance.hs+2−2

@@ -199,7 +199,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

199199 lamBind i (PPi _ n ty sc) sc'

200200 = PLam fc (sMN i "meth") Placeholder (lamBind (i+1) sc sc')

201201 lamBind i _ sc = sc

202− methArgs i (PPi (Imp _ _ _) n ty sc)

202+ methArgs i (PPi (Imp _ _ _ _) n ty sc)

203203 = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc

204204 methArgs i (PPi (Exp _ _ _) n ty sc)

205205 = PExp 0 [] (sMN 0 "marg") (PRef fc (sMN i "meth")) : methArgs (i+1) sc

@@ -230,7 +230,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

230230 conbind [] x = x

231231

232232 coninsert :: [(Name, PTerm)] -> PTerm -> PTerm

233− coninsert cs (PPi p@(Imp _ _ _) n t sc) = PPi p n t (coninsert cs sc)

233+ coninsert cs (PPi p@(Imp _ _ _ _) n t sc) = PPi p n t (coninsert cs sc)

234234 coninsert cs sc = conbind cs sc

235235

236236 insertDefaults :: IState -> Name ->

src/Idris/Elab/Record.hs+4−4

@@ -130,13 +130,13 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty_in

130130-- ++ "\n" ++ pshow i v

131131 putIState i)

132132

133− getBoundImpls (PPi (Imp _ _ _) n ty sc) = (n, ty) : getBoundImpls sc

133+ getBoundImpls (PPi (Imp _ _ _ _) n ty sc) = (n, ty) : getBoundImpls sc

134134 getBoundImpls _ = []

135135

136− getImplB k (PPi (Imp l s _) n Placeholder sc)

136+ getImplB k (PPi (Imp l s _ _) n Placeholder sc)

137137 = getImplB k sc

138− getImplB k (PPi (Imp l s p) n ty sc)

139− = getImplB (\x -> k (PPi (Imp l s p) n ty x)) sc

138+ getImplB k (PPi (Imp l s p fa) n ty sc)

139+ = getImplB (\x -> k (PPi (Imp l s p fa) n ty x)) sc

140140 getImplB k (PPi _ n ty sc)

141141 = getImplB k sc

142142 getImplB k _ = k

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

@@ -104,11 +104,11 @@ 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 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

111− param_pos i ns (Bind n (Pi t _) sc)

111+ param_pos i ns (Bind n (Pi _ t _) sc)

112112 | n `elem` ns = i : param_pos (i + 1) ns sc

113113 | otherwise = param_pos (i + 1) ns sc

114114 param_pos i ns t = []

@@ -196,7 +196,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

196196 lst = txt "List"

197197 errrep = txt "ErrorReportPart"

198198

199− tyIsHandler (Bind _ (Pi (P _ (NS (UN e) ns1) _) _)

199+ tyIsHandler (Bind _ (Pi _ (P _ (NS (UN e) ns1) _) _)

200200 (App (P _ (NS (UN m) ns2) _)

201201 (App (P _ (NS (UN l) ns3) _)

202202 (P _ (NS (UN r) ns4) _))))

src/Idris/Elab/Utils.hs+6−6

@@ -49,14 +49,14 @@ checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

4949-- Get the list of (index, name) of inaccessible arguments from an elaborated

5050-- type

5151inaccessibleImps :: Int -> Type -> [Bool] -> [(Int, Name)]

52−inaccessibleImps i (Bind n (Pi t _) sc) (inacc : ins)

52+inaccessibleImps i (Bind n (Pi _ t _) sc) (inacc : ins)

5353 | inacc = (i, n) : inaccessibleImps (i + 1) sc ins

5454 | otherwise = inaccessibleImps (i + 1) sc ins

5555inaccessibleImps _ _ _ = []

5656

5757-- Get the list of (index, name) of inaccessible arguments from the type.

5858inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]

59−inaccessibleArgs i (PPi (Imp _ _ _) n Placeholder t)

59+inaccessibleArgs i (PPi (Imp _ _ _ _) n Placeholder t)

6060 = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit

6161inaccessibleArgs i (PPi plicity n ty t)

6262 | InaccessibleArg `elem` pargopts plicity

@@ -155,13 +155,13 @@ psolve tm = return ()

155155pvars ist (Bind n (PVar t) sc) = (n, delab ist t) : pvars ist sc

156156pvars ist _ = []

157157

158−getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t _) sc)

158+getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi _ t _) sc)

159159 = nub $ getFixedInType i env [] t ++

160160 getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

161161 ++ case t of

162162 P _ n _ -> if n `elem` env then [n] else []

163163 _ -> []

164−getFixedInType i env (_ : is) (Bind n (Pi t _) sc)

164+getFixedInType i env (_ : is) (Bind n (Pi _ t _) sc)

165165 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

166166getFixedInType i env is tm@(App f a)

167167 | (P _ tn _, args) <- unApply tm

@@ -175,7 +175,7 @@ getFixedInType i env is tm@(App f a)

175175 getFixedInType i env is a

176176getFixedInType i _ _ _ = []

177177

178−getFlexInType i env ps (Bind n (Pi t _) sc)

178+getFlexInType i env ps (Bind n (Pi _ t _) sc)

179179 = nub $ (if (not (n `elem` ps)) then getFlexInType i env ps t else []) ++

180180 getFlexInType i (n : env) ps (instantiate (P Bound n t) sc)

181181getFlexInType i env ps tm@(App f a)

@@ -256,7 +256,7 @@ getStaticNames ist tm

256256getStaticNames _ _ = []

257257

258258getStatics :: [Name] -> Term -> [Bool]

259−getStatics ns (Bind n (Pi _ _) t)

259+getStatics ns (Bind n (Pi _ _ _) t)

260260 | n `elem` ns = True : getStatics ns t

261261 | otherwise = False : getStatics ns t

262262getStatics _ _ = []

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 (TType (UVar (-2))) (TType (UVar (-1))))

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

108− (Bind (sUN "x") (Pi (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 (TType (UVar (-3))) (TType (UVar (-2))))

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

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

132− (Bind (sUN "y") (Pi (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+48−17

@@ -152,7 +152,7 @@ getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon

152152 Nothing -> []

153153 Just ty -> checkArgs [] [] ty

154154 where checkArgs :: [Name] -> [[Name]] -> Type -> [Bool]

155− checkArgs env ns (Bind n (Pi t _) sc)

155+ checkArgs env ns (Bind n (Pi _ t _) sc)

156156 = let env' = case t of

157157 TType _ -> n : env

158158 _ -> env in

@@ -244,7 +244,8 @@ elab ist info emode opts fn tm

244244 then solveAuto ist fn False a

245245 else return ()) as

246246

247− ct <- insertCoerce ina t

247+ itm <- if not pattern then insertImpLam t else return t

248+ ct <- insertCoerce ina itm

248249 t' <- insertLazy ct

249250 g <- goal

250251 tm <- get_term

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

434435 bindable (UN xs) = True

435436 bindable n = implicitable n

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

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

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

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

439440 && isTConName n (tt_ctxt ist)

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

441442 | pattern && not reflection && e_nomatching ina

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

443− | 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 [])

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

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

446454 ctxt <- get_context

@@ -468,17 +476,17 @@ elab ist info emode opts fn tm

468476 elabE (ec { e_inarg = True, e_intype = True }) (Just fc) ty

469477 elabE (ec { e_inarg = True }) (Just fc) sc

470478 solve

471− elab' ina fc (PPi _ n Placeholder sc)

472− = do attack; arg n (sMN 0 "ty")

479+ elab' ina fc (PPi p n Placeholder sc)

480+ = do attack; arg n (is_scoped p) (sMN 0 "ty")

473481 elabE (ina { e_inarg = True, e_intype = True }) fc sc

474482 solve

475− elab' ina fc (PPi _ n ty sc)

483+ elab' ina fc (PPi p n ty sc)

476484 = do attack; tyn <- getNameFrom (sMN 0 "ty")

477485 claim tyn RType

478486 n' <- case n of

479487 MN _ _ -> unique_hole n

480488 _ -> return n

481− forall n' (Var tyn)

489+ forall n' (is_scoped p) (Var tyn)

482490 focus tyn

483491 let ec' = ina { e_inarg = True, e_intype = True }

484492 elabE ec' fc ty

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

564572 ans <- claimArgTys env xs

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

566574 fnTy [] ret = forget ret

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

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

568576

569577 localVar env (PRef _ x)

570578 = case lookup x env of

@@ -594,23 +602,25 @@ elab ist info emode opts fn tm

594602-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty && not qq

595603-- = lift $ tfail (Msg "Typecase is not allowed")

596604 -- if f is local, just do a simple_app

597− elab' ina _ tm@(PApp fc (PRef _ f) args)

605+ elab' ina _ tm@(PApp fc (PRef _ f) args_in)

598606 | pattern && not reflection && e_nomatching ina

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

600608 | otherwise

601609 = do env <- get_env

602610 ty <- goal

611+ fty <- get_type (Var f)

603612 ctxt <- get_context

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

604614 let unmatchableArgs = if pattern

605615 then getUnmatchable (tt_ctxt ist) f

606616 else []

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

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

609−

619+

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

611621 && isTConName f (tt_ctxt ist)) $

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

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

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

614624 then -- simple app, as below

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

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

@@ -1049,6 +1059,27 @@ elab ist info emode opts fn tm

10491059 notImplicitable (PCase _ _ _) = True

10501060 notImplicitable _ = False

10511061

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

1070+

1071+ insertImpLam t =

1072+ do ty <- goal

1073+ env <- get_env

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

1075+ addLam ty' t

1076+ where

1077+ -- just one level at a time

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

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

1080+ return (PLam emptyFC impn Placeholder t)

1081+ addLam _ t = return t

1082+

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

10531084 insertCoerce ina t | notImplicitable t = return t

10541085 insertCoerce ina t =

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

15161547 where tacticTy = Var (reflm "Tactic")

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

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

1519− (Pi (RApp listTy envTupleType) RType)

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

15201551 (RBind (sMN 1 "__pi_arg")

1521− (Pi (Var $ reflm "TT") RType) tacticTy))

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

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

15231554 -- goal, then apply the resulting reflected Tactic

15241555 = do tgoal <- goal

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

17911822reifyTTBinderApp reif f [t]

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

17931824reifyTTBinderApp reif f [t, k]

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

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

17951826reifyTTBinderApp reif f [x, y]

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

17971828reifyTTBinderApp reif f [x, y]

@@ -1934,7 +1965,7 @@ reflectQuotePattern unq (Bind n b x)

19341965 fill $ reflCall "Lam" [Var (reflm "TT"), Var t']

19351966 solve

19361967 focus t'; reflectQuotePattern unq t

1937− reflectBinderQuotePattern unq (Pi t k)

1968+ reflectBinderQuotePattern unq (Pi _ t k)

19381969 = do t' <- claimTT (sMN 0 "ty") ; movelast t'

19391970 k' <- claimTT (sMN 0 "k"); movelast k';

19401971 fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']

@@ -2084,7 +2115,7 @@ reflectBinder = reflectBinderQuote []

20842115reflectBinderQuote :: [Name] -> Binder Term -> Raw

20852116reflectBinderQuote unq (Lam t)

20862117 = reflCall "Lam" [Var (reflm "TT"), reflectQuote unq t]

2087−reflectBinderQuote unq (Pi t k)

2118+reflectBinderQuote unq (Pi _ t k)

20882119 = reflCall "Pi" [Var (reflm "TT"), reflectQuote unq t, reflectQuote unq k]

20892120reflectBinderQuote unq (Let x y)

20902121 = reflCall "Let" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]

src/Idris/Erasure.hs+1−1

@@ -354,7 +354,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

354354 -- here we just push IM.empty on the de bruijn stack

355355 -- the args will be marked as used at the usage site

356356 | Lam ty <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd body

357− | Pi ty _ <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd body

357+ | Pi _ ty _ <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd body

358358

359359 -- let-bound variables can get partially evaluated

360360 -- it is sufficient just to plug the Cond in when the bound names are used

src/Idris/IBC.hs+5−3

@@ -35,7 +35,7 @@ import Codec.Compression.Zlib (compress)

3535import Util.Zlib (decompressEither)

3636

3737ibcVersion :: Word8

38−ibcVersion = 92

38+ibcVersion = 93

3939

4040data IBCFile = IBCFile { ver :: Word8,

4141 sourcefile :: FilePath,

@@ -1111,11 +1111,12 @@ instance Binary Static where

11111111instance Binary Plicity where

11121112 put x

11131113 = case x of

1114− Imp x1 x2 x3 ->

1114+ Imp x1 x2 x3 x4 ->

11151115 do putWord8 0

11161116 put x1

11171117 put x2

11181118 put x3

1119+ put x4

11191120 Exp x1 x2 x3 ->

11201121 do putWord8 1

11211122 put x1

@@ -1136,7 +1137,8 @@ instance Binary Plicity where

11361137 0 -> do x1 <- get

11371138 x2 <- get

11381139 x3 <- get

1139− return (Imp x1 x2 x3)

1140+ x4 <- get

1141+ return (Imp x1 x2 x3 x4)

11401142 1 -> do x1 <- get

11411143 x2 <- get

11421144 x3 <- get

src/Idris/Interactive.hs+4−4

@@ -299,10 +299,10 @@ makeLemma fn updatefile l n

299299 where getIndent s = length (takeWhile isSpace s)

300300

301301 appArgs skip 0 _ = ""

302− appArgs skip i (Bind n@(UN c) (Pi _ _) sc)

302+ appArgs skip i (Bind n@(UN c) (Pi _ _ _) sc)

303303 | (thead c /= '_' && n `notElem` skip)

304304 = " " ++ show n ++ appArgs skip (i - 1) sc

305− appArgs skip i (Bind _ (Pi _ _) sc) = appArgs skip (i - 1) sc

305+ appArgs skip i (Bind _ (Pi _ _ _) sc) = appArgs skip (i - 1) sc

306306 appArgs skip i _ = ""

307307

308308 stripMNBind skip (PPi b n@(UN c) ty sc)

@@ -316,7 +316,7 @@ makeLemma fn updatefile l n

316316 -- Make them implicit if they appear guarded by a top level constructor,

317317 -- or at the top level themselves.

318318 guessImps :: Context -> Term -> [Name]

319− guessImps ctxt (Bind n (Pi _ _) sc)

319+ guessImps ctxt (Bind n (Pi _ _ _) sc)

320320 | guarded ctxt n (substV (P Bound n Erased) sc)

321321 = n : guessImps ctxt sc

322322 | otherwise = guessImps ctxt sc

@@ -328,7 +328,7 @@ makeLemma fn updatefile l n

328328 isConName f ctxt = any (guarded ctxt n) args

329329-- guarded ctxt n (Bind (UN cn) (Pi t) sc) -- ignore shadows

330330-- | thead cn /= '_' = guarded ctxt n t || guarded ctxt n sc

331− guarded ctxt n (Bind _ (Pi t _) sc)

331+ guarded ctxt n (Bind _ (Pi _ t _) sc)

332332 = guarded ctxt n t || guarded ctxt n sc

333333 guarded ctxt n _ = False

334334

src/Idris/ParseExpr.hs+30−17

@@ -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,14 +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− if implicitAllowed syn

886− then return (bindList (PPi (Imp opts st False)) xt sc)

887− else fail "no implicit arguments allowed here"))

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

888898 <|> (do x <- opExpr syn

889− (do symbol "->"

899+ (do binder <- bindsymbol opts st syn

890900 sc <- expr syn

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

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

892902 <|> return x)

893903 <?> "dependent type signature"

894904

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

913923@

914924-}

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

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

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

918− lchar ')'

919− reservedOp "=>"

920− return tys)

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

922− reservedOp "=>"

923− return [(defname, t)])

924− <|> return []

925− <?> "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"

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

927940 e <- expr' (disallowImp syn)

928941 return (n, e))

src/Idris/PartialEval.hs+12−12

@@ -85,35 +85,35 @@ specType args ty = let (t, args') = runState (unifyEq args ty) [] in

8585 where

8686 -- Specialise static argument in type by let-binding provided value instead

8787 -- of expecting it as a function argument

88− st ((ExplicitS, v) : xs) (Bind n (Pi t _) sc)

88+ st ((ExplicitS, v) : xs) (Bind n (Pi _ t _) sc)

8989 = Bind n (Let t v) (st xs sc)

90− st ((ImplicitS, v) : xs) (Bind n (Pi t _) sc)

90+ st ((ImplicitS, v) : xs) (Bind n (Pi _ t _) sc)

9191 = Bind n (Let t v) (st xs sc)

9292 -- Erase argument from function type

93− st ((UnifiedD, _) : xs) (Bind n (Pi t _) sc)

93+ st ((UnifiedD, _) : xs) (Bind n (Pi _ t _) sc)

9494 = st xs sc

9595 -- Keep types as is

96− st (_ : xs) (Bind n (Pi t k) sc)

97− = Bind n (Pi t k) (st xs sc)

96+ st (_ : xs) (Bind n (Pi i t k) sc)

97+ = Bind n (Pi i t k) (st xs sc)

9898 st _ t = t

9999

100100 -- Erase implicit dynamic argument if existing argument shares it value,

101101 -- by substituting the value of previous argument

102− unifyEq (imp@(ImplicitD, v) : xs) (Bind n (Pi t k) sc)

102+ unifyEq (imp@(ImplicitD, v) : xs) (Bind n (Pi i t k) sc)

103103 = do amap <- get

104104 case lookup imp amap of

105105 Just n' ->

106106 do put (amap ++ [((UnifiedD, Erased), n)])

107107 sc' <- unifyEq xs (subst n (P Bound n' Erased) sc)

108− return (Bind n (Pi t k) sc') -- erase later

108+ return (Bind n (Pi i t k) sc') -- erase later

109109 _ -> do put (amap ++ [(imp, n)])

110110 sc' <- unifyEq xs sc

111− return (Bind n (Pi t k) sc')

112− unifyEq (x : xs) (Bind n (Pi t k) sc)

111+ return (Bind n (Pi i t k) sc')

112+ unifyEq (x : xs) (Bind n (Pi i t k) sc)

113113 = do args <- get

114114 put (args ++ [(x, n)])

115115 sc' <- unifyEq xs sc

116− return (Bind n (Pi t k) sc')

116+ return (Bind n (Pi i t k) sc')

117117 unifyEq xs t = do args <- get

118118 put (args ++ (zip xs (repeat (sUN "_"))))

119119 return t

@@ -127,9 +127,9 @@ specType args ty = let (t, args') = runState (unifyEq args ty) [] in

127127mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Type -> PTerm

128128mkPE_TyDecl ist args ty = mkty args ty

129129 where

130− mkty ((ExplicitD, v) : xs) (Bind n (Pi t k) sc)

130+ mkty ((ExplicitD, v) : xs) (Bind n (Pi _ t k) sc)

131131 = PPi expl n (delab ist (generaliseIn t)) (mkty xs sc)

132− mkty ((ImplicitD, v) : xs) (Bind n (Pi t k) sc)

132+ mkty ((ImplicitD, v) : xs) (Bind n (Pi _ t k) sc)

133133 | concreteClass ist t = mkty xs sc

134134 | classConstraint ist t

135135 = PPi constraint n (delab ist (generaliseIn t)) (mkty xs sc)

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 (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/REPL.hs+1−1

@@ -402,7 +402,7 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.Metavariables cols) =

402402 -- | Split a function type into a pair of premises, conclusion.

403403 -- Each maintains both the original and delaborated versions.

404404 splitPi :: IState -> Type -> ([(Name, Type, PTerm)], Type, PTerm)

405− splitPi ist (Bind n (Pi t _) rest) =

405+ splitPi ist (Bind n (Pi _ t _) rest) =

406406 let (hs, c, pc) = splitPi ist rest in

407407 ((n, t, delabTy' ist [] t False False):hs,

408408 c, delabTy' ist [] c False False)

src/Idris/TypeSearch.hs+2−2

@@ -120,7 +120,7 @@ computeDagP removePred t = (reverse (map f arguments), reverse theRemovedArgs ,

120120 (arguments, theRemovedArgs, retTy) = go [] [] t

121121

122122 -- NOTE : args are in reverse order

123− go args removedArgs (Bind n (Pi ty _) sc) = let arg = (n, ty) in

123+ go args removedArgs (Bind n (Pi _ ty _) sc) = let arg = (n, ty) in

124124 if removePred ty

125125 then go args (arg : removedArgs) sc

126126 else go (arg : args) removedArgs sc

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