9ec3ec7 · Idris-dev · git.iko.soy

CHANGELOG+3

compare with master

unifiedsplit

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

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

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

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

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

6+ the top level.

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

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

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

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

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

7 the names exported from that module.

10 the names exported from that module.

idris.cabal+3

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

321 test/basic011/run

322 test/basic011/*.idr

323 test/basic011/expected

324+ test/basic012/run

325+ test/basic012/*.idr

326+ test/basic012/expected

324

327

325 test/buffer001-disabled/*.idr

328 test/buffer001-disabled/*.idr

326 test/buffer001-disabled/run

329 test/buffer001-disabled/run

src/Idris/AbsSyntax.hs+16−15

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

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

1125 addIBC (IBCStatic n)

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

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

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

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

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

1133 else if (not (searchArg p))

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

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

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

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

1147 = n : getParamNames ist sc

1148 getParamNames ist _ = []

1149

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

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

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

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

1153 getNamesFrom i ps sc = []

1154

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

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

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

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

1158 concatMap freeNames args

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

1164 searchArg (TacImp _ _ _) = True

1165 searchArg _ = False

1166

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

1168 staticList _ _ = []

1169

1170-- Dealing with implicit arguments

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

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

1243 doAdd (UImplicit n ty : cs) ns t

1244 | elem n ns

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

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

1246 | otherwise = doAdd cs ns t

1247

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

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

1250 bindFree (n:ns) tm

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

1252 | otherwise

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

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

1254

1255 getArgnames (PPi _ n c sc)

1256 = n : getArgnames sc

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

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

1266 collectImps _ = []

1267

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

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

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

1270 where

1271 where

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

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

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

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

1273 argInfo n (Exp opt _ _) t'

1274 argInfo n (Exp opt _ _) t'

1274 = (InaccessibleArg `elem` opt,

1275 = (InaccessibleArg `elem` opt,

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

1279 argInfo n (TacImp opt _ scr) t'

1280 argInfo n (TacImp opt _ scr) t'

1280 = (InaccessibleArg `elem` opt,

1281 = (InaccessibleArg `elem` opt,

1281 PTacImplicit 10 opt n scr t')

1282 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

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

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

1284 getImps sc tm = []

1285 getImps sc tm = []

1285

1286

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

1358 = do (decls, ns) <- get

1359 = do (decls, ns) <- get

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

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

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

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

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

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

1363 (decls , ns) <- get

1364 (decls , ns) <- get

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

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

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

1426 pibind using [] sc = sc

1427 pibind using [] sc = sc

1427 pibind using (n:ns) sc

1428 pibind using (n:ns) sc

1428 = case lookup n using of

1429 = case lookup n using of

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

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

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

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

1431 (pibind using ns sc)

1432 (pibind using ns sc)

1432

1433

1433-- Add implicit arguments in function calls

1434-- Add implicit arguments in function calls

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

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

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

1712 su :: PTerm -> PTerm

1713 su :: PTerm -> PTerm

1713 su (PRef fc f)

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

1715 = Placeholder

1716 = Placeholder

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

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

1717 | isDConName fn ctxt

1718 | isDConName fn ctxt

src/Idris/AbsSyntaxTree.hs+12−4

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

488-- Mark bindings with their explicitness, and laziness

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

490 pstatic :: Static,

491− pparam :: Bool }

491+ pparam :: Bool,

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

493+ }

492 | Exp { pargopts :: [ArgOpt],

494 | Exp { pargopts :: [ArgOpt],

493 pstatic :: Static,

495 pstatic :: Static,

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

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

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

504deriving instance NFData Plicity

506deriving instance NFData Plicity

505!-}

507!-}

506

508

509+is_scoped :: Plicity -> Maybe ImplicitInfo

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

511+is_scoped _ = Nothing

512+

507−impl = Imp [] Dynamic False

513+impl = Imp [] Dynamic False Nothing

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

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

508expl = Exp [] Dynamic False

516expl = Exp [] Dynamic False

509expl_param = Exp [] Dynamic True

517expl_param = Exp [] Dynamic True

510constraint = Constraint [] Static

518constraint = Constraint [] Static

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

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

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

1141

1149

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

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

1144 toTy (PVar t) = PVTy t

1152 toTy (PVar t) = PVTy t

1145 toTy b = b

1153 toTy b = b

1146getInferType (App (App _ ty) _) = ty

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

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

1326 case s of

1334 case s of

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

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

1328 _ -> empty

1336 _ -> empty

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

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

1330 | ppopt_impl ppo =

1338 | ppopt_impl ppo =

1331 bracket p startPrec $

1339 bracket p startPrec $

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

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

src/Idris/Apropos.hs+1−1

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

66

67instance Apropos (Binder (TT Name)) where

68 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

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

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

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

183 = case lookupTy n (tt_ctxt ist) of

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

185 _ -> repeat Nothing

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

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

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

188 | otherwise = Nothing

189argTys _ _ = repeat Nothing

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

@@ -403,15 +403,23 @@ instance Binary Raw where

403 return (RUType x1)

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

405

406+instance Binary ImplicitInfo where

407+ put x

408+ = case x of

409+ Impl x1 -> put x1

410+ get

411+ = do x1 <- get

412+ return (Impl x1)

406

413

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

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

408 put x

415 put x

409 = case x of

416 = case x of

410 Lam x1 -> do putWord8 0

417 Lam x1 -> do putWord8 0

411 put x1

418 put x1

412− Pi x1 x2 -> do putWord8 1

419+ Pi x1 x2 x3 -> do putWord8 1

413− put x1

420+ put x1

414− put x2

421+ put x2

422+ put x3

415 Let x1 x2 -> do putWord8 2

423 Let x1 x2 -> do putWord8 2

416 put x1

424 put x1

417 put x2

425 put x2

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

437 return (Lam x1)

445 return (Lam x1)

438 1 -> do x1 <- get

446 1 -> do x1 <- get

439 x2 <- get

447 x2 <- get

448+ x3 <- get

440− return (Pi x1 x2)

449+ return (Pi x1 x2 x3)

441 2 -> do x1 <- get

450 2 -> do x1 <- get

442 x2 <- get

451 x2 <- get

443 return (Let x1 x2)

452 return (Let x1 x2)

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

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

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

371 | otherwise = PConst x

372

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

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

374 | reflect && noOccurrence n sc

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

376

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

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

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

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

91

92+instance NFData ImplicitInfo where

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

94+

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

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

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

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

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

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

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

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

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

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

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

100 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

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

269 isInj ctxt (Constant _) = True

270 isInj ctxt (TType _) = True

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

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

272 isInj ctxt _ = False

273

274-- get instance argument names

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

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

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

371

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

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

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

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

374

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

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

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

493 env <- get_env

494 -- let claims = getArgs ty imps

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

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

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

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

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

499 let n = length (filter not imps)

501 let n = length (filter not imps)

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

502 return $! claims

504 return $! claims

503 where

505 where

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

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

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

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

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

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

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

507 -> [Name] -- ^ Hypotheses

510 -> [Name] -- ^ Hypotheses

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

511 -> 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 =

510 do let t = rebind hs t_in

513 do let t = rebind hs t_in

511 n <- getNameFrom (mkMN n')

514 n <- getNameFrom (mkMN n')

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

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

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

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

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

515 claim n (forget t)

518 claim n (forget t)

516 when i (movelast n)

519 when i (movelast n)

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

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

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

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

519− mkClaims _ _ _ _

524+ mkClaims _ _ _ _ _

520 | Var n <- fn

525 | Var n <- fn

521 = do ctxt <- get_context

526 = do ctxt <- get_context

522 case lookupTy n ctxt of

527 case lookupTy n ctxt of

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

614 priOrder _ Nothing = GT

619 priOrder _ Nothing = GT

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

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

616

621

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

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

618 do n <- unique_hole (mkMN n')

623 do n <- unique_hole (mkMN n')

619 when (null claims) (start_unify n)

624 when (null claims) (start_unify n)

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

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

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

649checkPiGoal n

654checkPiGoal n

650 = do g <- goal

655 = do g <- goal

651 case g of

656 case g of

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

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

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

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

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

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

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

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

656 claim a RType

661 claim a RType

657 claim b RType

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

659 movelast a

664 movelast a

660 movelast b

665 movelast b

661 fill (Var f)

666 fill (Var f)

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

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

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

671 claim a RType

676 claim a RType

672 claim b RType

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

674 tm <- get_term

679 tm <- get_term

675 start_unify s

680 start_unify s

676 claim s (Var a)

681 claim s (Var a)

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

693

698

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

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

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

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

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

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

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

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

698− claim ty RType

703+ claim ty RType

699− movelast ty

704+ movelast ty

700− forall n (Var ty)

705+ forall n i (Var ty)

701

706

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

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

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

708no_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

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

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

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

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

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

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

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

602 where

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

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

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

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

608 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

88 b' <- fixBinder b

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

90 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

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

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

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

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

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

69 | CheckIn Raw

70 | Intro (Maybe Name)

71 | IntroTy Raw (Maybe Name)

72− | Forall Name Raw

72+ | Forall Name (Maybe ImplicitInfo) Raw

73 | LetBind Name Raw Raw

74 | ExpandLet Name Term

75 | Rewrite Raw

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

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

413 where

414 mkTy [] t = t

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

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

416

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

418

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

540 Just name -> name

541 Nothing -> x

542 let t' = case t of

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

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

544 _ -> hnf ctxt env t

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

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

547 case t' of

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

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

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

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

550− ps <- get

550+ ps <- get

551− let (uh, uns) = unified ps

551+ let (uh, uns) = unified ps

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

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

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

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

554 _ -> lift $ tfail $ CantIntroduce t'

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

556

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

560 Just name -> name

561 Nothing -> x

562 let t' = case t of

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

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

564 _ -> hnf ctxt env t

565 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') $

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

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

569 _ -> lift $ tfail $ CantIntroduce t'

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

571

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

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

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

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

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

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

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

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

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

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

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

579

580patvar :: Name -> RunTactic

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

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

973 mktac HNF_Compute = hnf_compute

974 mktac (Intro n) = intro n

975 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

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

978 mktac (ExpandLet n b) = expandLet n b

979 mktac (Rewrite t) = rewrite t

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

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

672deriving instance NFData Raw

673!-}

674

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

676+ deriving (Show, Eq, Ord)

677+

678+{-!

679+deriving instance Binary ImplicitInfo

680+deriving instance NFData ImplicitInfo

681+!-}

682+

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

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

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

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

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

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

@@ -679,9 +687,13 @@ deriving instance NFData Raw

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

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

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

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

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

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

690+ | Pi { binderImpl :: Maybe ImplicitInfo,

682− | Pi { binderTy :: !b,

691+ binderTy :: !b,

683 binderKind :: !b }

692 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. -}

685 | Let { binderTy :: !b,

697 | Let { binderTy :: !b,

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

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

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

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

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

703

715

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

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

705 size (Lam ty) = 1 + size ty

717 size (Lam ty) = 1 + size ty

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

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

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

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

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

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

709 size (Hole ty) = 1 + size ty

721 size (Hole ty) = 1 + size ty

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

885isInjective (Constant _) = True

897isInjective (Constant _) = True

886isInjective (TType x) = True

898isInjective (TType x) = True

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

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

888isInjective (App f a) = isInjective f

900isInjective (App f a) = isInjective f

889isInjective _ = False

901isInjective _ = False

890

902

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

1099

1111

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

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

1101arity :: TT n -> Int

1113arity :: TT n -> Int

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

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

1103arity _ = 0

1115arity _ = 0

1104

1116

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

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

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

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

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

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

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

1173getArgTys (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

1163getArgTys _ = []

1175getArgTys _ = []

1164

1176

1165getRetTy :: TT n -> TT n

1177getRetTy :: TT n -> TT n

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

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

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

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

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

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

1169getRetTy sc = sc

1181getRetTy sc = sc

1170

1182

1171uniqueNameFrom :: [Name] -> [Name] -> Name

1183uniqueNameFrom :: [Name] -> [Name] -> Name

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

1281 else

1293 else

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

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

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

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

1285 | noOccurrence n sc && not debug =

1297 | noOccurrence n sc && not debug =

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

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

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

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

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

1297 -- Render a `Binder` and its name

1309 -- Render a `Binder` and its name

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

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

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

1311 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

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

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

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

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

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

1315 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1353 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

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

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

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

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

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

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

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

1399

1411

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

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

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

1413 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

1403 op ps sc = bindAll (sortP ps) sc

1415 op ps sc = bindAll (sortP ps) sc

1404

1416

1405 sortP ps = pick [] (reverse ps)

1417 sortP ps = pick [] (reverse ps)

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

1445 v' <- getPats v

1457 v' <- getPats v

1446 sc' <- getPats sc

1458 sc' <- getPats sc

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

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

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

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

1449− k' <- getPats k

1461+ k' <- getPats k

1450− sc' <- getPats sc

1462+ sc' <- getPats sc

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

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

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

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

1453 sc' <- getPats sc

1465 sc' <- getPats sc

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

1466 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

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

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

89 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

91 _ -> uniqueBinders (map fst env)

92 $ 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

94 _ -> normalise ctxt env fty

95 case fty' of

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

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

97 do convertsC ctxt env aty s

98 let apty = simplify initContext env

99 (Bind x (Let aty av) t)

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

133 constType _ = TType (UVal 0)

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

135 return (Erased, ty)

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

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

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

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

140 (v, cs) <- get

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

142 (TType su, TType tu) -> do

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

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

146 (pToV n tv), k')

147 (un, un') ->

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

150 (pToV n tv), k')

151

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

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

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

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

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

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

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

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

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

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

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

166

167 chk u env (RBind n b sc)

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

230 return (PVTy tv, tt')

231

232 discharge n (Lam t) bt scv sct

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

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

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

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

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

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

236 discharge n (Let t v) bt scv sct

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

238 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 =

86 return (map (renameBinders env) v')

87 _ -> tfail e

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

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

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

94 StateT UInfo

90 StateT UInfo

95 TC [(Name, TT Name)]

91 TC [(Name, TT Name)]

96

92

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)

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

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

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

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

99 holeIn env f || f `elem` holes

109 holeIn env f || f `elem` holes

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

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

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

111 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

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

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

104 holeIn env f || f `elem` holes

114 holeIn env f || f `elem` holes

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

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

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

143 h2 <- un bnames vx vy

153 h2 <- un bnames vx vy

144 combine bnames h1 h2

154 combine bnames h1 h2

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

155 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

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

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

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

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

149 (normalise ctxt env (binderTy y))

159 (normalise ctxt env (binderTy y))

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

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

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

432 -- class resolution for type classes over functions.

442 -- class resolution for type classes over functions.

433

443

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)

435 | noOccurrence n y && injectiveApp f

445 | noOccurrence n y && injectiveApp f

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

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

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

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

439 combine bnames ux uf

449 combine bnames ux uf

440

450

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)

442 | noOccurrence n y && injectiveApp f

452 | noOccurrence n y && injectiveApp f

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

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

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

454 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

446 combine bnames ux uf

456 combine bnames ux uf

447

457

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

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

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

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

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

452 combine bnames h1 h2

462 combine bnames h1 h2

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

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

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

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

455 sameBinder _ _ = False

465 sameBinder _ _ = False

456 un' fn bnames x y

466 un' fn bnames x y

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

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

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

583 sc 1

593 sc 1

584 combine bnames h1 h2

594 combine bnames h1 h2

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

595 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

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

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

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

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

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

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

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

686 | f == f' = recoverable a a'

696 | f == f' = recoverable a a'

687recoverable (App f a) (App f' a')

697recoverable (App f a) (App f' a')

688 = recoverable f f' -- && recoverable a a'

698 = recoverable f f' -- && recoverable a a'

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

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

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

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

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

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

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

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

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

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

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

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

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

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

src/Idris/Coverage.hs+4−4

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

286 where

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

288

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

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

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

291 n' `elem` mut_ns = all noRec args

292 cp _ = True

293

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

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

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

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

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

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

536 = case lookupTy n (tt_ctxt ist) of

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

538 _ -> args

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

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

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

541 expand i _ xs = xs

542

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

src/Idris/DeepSeq.hs+2−2

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

94 rnf _ = ()

95

96instance NFData Plicity where

97− rnf (Imp x1 x2 x3)

97+ rnf (Imp x1 x2 x3 x4)

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

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

99 rnf (Exp x1 x2 x3)

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

101 rnf (Constraint x1 x2)

src/Idris/Delaborate.hs+13−8

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

57 _ -> PRef un n

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

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

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

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

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

61+ | tcinstance impl

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

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

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)

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)

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

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

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

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

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

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

68 n

73 n

69 (de env [] ty)

74 (de env [] ty)

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

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

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

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

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

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

73

78

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

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

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

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

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

223 y)) <>

228 y)) <>

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

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

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

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

228 flagUnique (App f a) = App (flagUnique f) (flagUnique a)

233 flagUnique (App f a) = App (flagUnique f) (flagUnique a)

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

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

230 flagUnique t = t

235 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

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

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

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

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

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

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

137 (n, (syn, o, t) ) )

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

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

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

139

140

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

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

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

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

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

202

203

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

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

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

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

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

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

206 getMArgs _ = []

207 getMArgs _ = []

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

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

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

219 rhsArgs [] _ = []

220 rhsArgs [] _ = []

220

221

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

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

222 = PPi p n ty (insertConstraint c sc)

223 = PPi p n ty (insertConstraint c sc)

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

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

224 (sMN 0 "class") c sc

225 (sMN 0 "class") c sc

225

226

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

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

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

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

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

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

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

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

867 let wargval = getRetTy cwvalN

868 let wargtype = getRetTy cwvaltyN

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

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

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

871 (sMN 0 "warg", wargtype) :

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

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

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

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

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

925 where

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

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

927 getImps _ = []

928

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

177 getDataApp f@(App _ _)

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

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

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

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

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

182 getDataApp _ = []

183

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

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

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

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

201 lamBind i _ sc = sc

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

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

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

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

205 = 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

230 conbind [] x = x

231

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

234 coninsert cs sc = conbind cs sc

235

236 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

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

131 putIState i)

132

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

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

134 getBoundImpls _ = []

135

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

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

137 = getImplB k sc

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

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

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

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

140 getImplB k (PPi _ n ty sc)

141 = getImplB k sc

142 getImplB k _ = k

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

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

104

105 return (cty, ckind, ty, inacc)

106 where

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

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

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

109 patToImp t = t

110

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

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

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

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

114 param_pos i ns t = []

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

196 lst = txt "List"

197 errrep = txt "ErrorReportPart"

198

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

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

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

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

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

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

50-- type

51inaccessibleImps :: 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)

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

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

55inaccessibleImps _ _ _ = []

56

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

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

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

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

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

61inaccessibleArgs i (PPi plicity n ty t)

62 | InaccessibleArg `elem` pargopts plicity

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

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

156pvars ist _ = []

157

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

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

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

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

161 ++ case t of

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

163 _ -> []

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

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

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

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

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

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

175 getFixedInType i env is a

176getFixedInType i _ _ _ = []

177

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

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

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

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

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

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

256getStaticNames _ _ = []

257

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

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

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

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

261 | otherwise = False : getStatics ns t

262getStatics _ _ = []

src/Idris/ElabDecls.hs+7−7

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

103

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

105 p_believeMe _ = Nothing

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

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

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

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

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

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

109 elabBelieveMe

110 = do let prim__believe_me = sUN "prim__believe_me"

111 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)

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

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

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

128

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

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

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

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

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

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

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

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

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

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

135 elabSynEq

src/Idris/ElabTerm.hs+48−17

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

152 Nothing -> []

153 Just ty -> checkArgs [] [] ty

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

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

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

156 = let env' = case t of

157 TType _ -> n : env

158 _ -> env in

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

244 then solveAuto ist fn False a

245 else return ()) as

246

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

247− ct <- insertCoerce ina t

248+ ct <- insertCoerce ina itm

248 t' <- insertLazy ct

249 t' <- insertLazy ct

249 g <- goal

250 g <- goal

250 tm <- get_term

251 tm <- get_term

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

434 bindable (UN xs) = True

435 bindable (UN xs) = True

435 bindable n = implicitable n

436 bindable n = implicitable n

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

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

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

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

439 && isTConName n (tt_ctxt ist)

440 && isTConName n (tt_ctxt ist)

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

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

441 | pattern && not reflection && e_nomatching ina

442 | pattern && not reflection && e_nomatching ina

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

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

444+ | otherwise =

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

446+ ctxt <- get_context

447+ env <- get_env

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

449+ if null a'

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

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

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

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

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

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

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

446 ctxt <- get_context

454 ctxt <- get_context

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

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

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

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

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

470 solve

478 solve

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

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

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

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

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

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

474 solve

482 solve

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

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

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

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

477 claim tyn RType

485 claim tyn RType

478 n' <- case n of

486 n' <- case n of

479 MN _ _ -> unique_hole n

487 MN _ _ -> unique_hole n

480 _ -> return n

488 _ -> return n

481− forall n' (Var tyn)

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

482 focus tyn

490 focus tyn

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

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

484 elabE ec' fc ty

492 elabE ec' fc ty

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

564 ans <- claimArgTys env xs

572 ans <- claimArgTys env xs

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

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

566 fnTy [] ret = forget ret

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

568

576

569 localVar env (PRef _ x)

577 localVar env (PRef _ x)

570 = case lookup x env of

578 = case lookup x env of

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

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

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

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

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

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

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

598 | pattern && not reflection && e_nomatching ina

606 | pattern && not reflection && e_nomatching ina

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

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

600 | otherwise

608 | otherwise

601 = do env <- get_env

609 = do env <- get_env

602 ty <- goal

610 ty <- goal

611+ fty <- get_type (Var f)

603 ctxt <- get_context

612 ctxt <- get_context

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

604 let unmatchableArgs = if pattern

614 let unmatchableArgs = if pattern

605 then getUnmatchable (tt_ctxt ist) f

615 then getUnmatchable (tt_ctxt ist) f

606 else []

616 else []

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

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

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

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

609−

619+

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

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

611 && isTConName f (tt_ctxt ist)) $

621 && isTConName f (tt_ctxt ist)) $

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

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

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

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

614 then -- simple app, as below

624 then -- simple app, as below

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

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

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

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

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

1049 notImplicitable (PCase _ _ _) = True

1059 notImplicitable (PCase _ _ _) = True

1050 notImplicitable _ = False

1060 notImplicitable _ = False

1051

1061

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+

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

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

1053 insertCoerce ina t | notImplicitable t = return t

1084 insertCoerce ina t | notImplicitable t = return t

1054 insertCoerce ina t =

1085 insertCoerce ina t =

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

1516 where tacticTy = Var (reflm "Tactic")

1547 where tacticTy = Var (reflm "Tactic")

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

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

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

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

1519− (Pi (RApp listTy envTupleType) RType)

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

1520 (RBind (sMN 1 "__pi_arg")

1551 (RBind (sMN 1 "__pi_arg")

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

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

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

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

1523 -- goal, then apply the resulting reflected Tactic

1554 -- goal, then apply the resulting reflected Tactic

1524 = do tgoal <- goal

1555 = do tgoal <- goal

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

1791reifyTTBinderApp reif f [t]

1822reifyTTBinderApp reif f [t]

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

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

1793reifyTTBinderApp reif f [t, k]

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

1795reifyTTBinderApp reif f [x, y]

1826reifyTTBinderApp reif f [x, y]

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

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

1797reifyTTBinderApp reif f [x, y]

1828reifyTTBinderApp reif f [x, y]

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

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

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

1935 solve

1966 solve

1936 focus t'; reflectQuotePattern unq t

1967 focus t'; reflectQuotePattern unq t

1937− reflectBinderQuotePattern unq (Pi t k)

1968+ reflectBinderQuotePattern unq (Pi _ t k)

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

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

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

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

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

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

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

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

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

2085reflectBinderQuote unq (Lam t)

2116reflectBinderQuote unq (Lam t)

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

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

2087−reflectBinderQuote unq (Pi t k)

2118+reflectBinderQuote unq (Pi _ t k)

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

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

2089reflectBinderQuote unq (Let x y)

2120reflectBinderQuote unq (Let x y)

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

2121 = 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]

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

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

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

358

359 -- let-bound variables can get partially evaluated

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

35import Util.Zlib (decompressEither)

36

37ibcVersion :: Word8

38−ibcVersion = 92

38+ibcVersion = 93

39

40data IBCFile = IBCFile { ver :: Word8,

41 sourcefile :: FilePath,

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

1111instance Binary Plicity where

1112 put x

1113 = case x of

1114− Imp x1 x2 x3 ->

1114+ Imp x1 x2 x3 x4 ->

1115 do putWord8 0

1116 put x1

1117 put x2

1118 put x3

1119+ put x4

1119 Exp x1 x2 x3 ->

1120 Exp x1 x2 x3 ->

1120 do putWord8 1

1121 do putWord8 1

1121 put x1

1122 put x1

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

1136 0 -> do x1 <- get

1137 0 -> do x1 <- get

1137 x2 <- get

1138 x2 <- get

1138 x3 <- get

1139 x3 <- get

1140+ x4 <- get

1139− return (Imp x1 x2 x3)

1141+ return (Imp x1 x2 x3 x4)

1140 1 -> do x1 <- get

1142 1 -> do x1 <- get

1141 x2 <- get

1143 x2 <- get

1142 x3 <- get

1144 x3 <- get

src/Idris/Interactive.hs+4−4

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

299 where getIndent s = length (takeWhile isSpace s)

300

301 appArgs skip 0 _ = ""

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

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

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

304 = " " ++ 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

306 appArgs skip i _ = ""

307

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

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

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

317 -- or at the top level themselves.

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

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

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

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

321 = n : guessImps ctxt sc

322 | otherwise = guessImps ctxt sc

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

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

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

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

332 = guarded ctxt n t || guarded ctxt n sc

333 guarded ctxt n _ = False

334

src/Idris/ParseExpr.hs+30−17

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

855@

856 -}

857

858+bindsymbol opts st syn

859+ = do symbol "->"

860+ return (Exp opts st False)

861+

858pi :: SyntaxInfo -> IdrisParser PTerm

862pi :: SyntaxInfo -> IdrisParser PTerm

859pi syn =

863pi syn =

860 do opts <- piOpts syn

864 do opts <- piOpts syn

861 st <- static

865 st <- static

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

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

863− symbol "->"

867+ binder <- bindsymbol opts st syn

864 sc <- expr syn

868 sc <- expr syn

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

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

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

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

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

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

868 xt <- typeDeclList syn

872 xt <- typeDeclList syn

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

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

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

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

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

883 symbol "->"

887 symbol "->"

888+ cs <- constraintList syn

884 sc <- expr syn

889 sc <- expr syn

890+ let (im,cl)

885− if implicitAllowed syn

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

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

896+ return (bindList (PPi im) xt

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

897+ (bindList (PPi cl) cs sc))))

888 <|> (do x <- opExpr syn

898 <|> (do x <- opExpr syn

889− (do symbol "->"

899+ (do binder <- bindsymbol opts st syn

890 sc <- expr syn

900 sc <- expr syn

891− return (PPi (Exp opts st False) (sUN "__pi_arg") x sc))

901+ return (PPi binder (sUN "__pi_arg") x sc))

892 <|> return x)

902 <|> return x)

893 <?> "dependent type signature"

903 <?> "dependent type signature"

894

904

@@ -913,16 +923,19 @@ ConstraintList ::=

913@

923@

914-}

924-}

915constraintList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]

925constraintList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]

916−constraintList syn = try (do lchar '('

926+constraintList syn = try (constraintList1 syn)

927+ <|> return []

928+

929+constraintList1 :: SyntaxInfo -> IdrisParser [(Name, PTerm)]

930+constraintList1 syn = try (do lchar '('

917− tys <- sepBy1 nexpr (lchar ',')

931+ tys <- sepBy1 nexpr (lchar ',')

918− lchar ')'

932+ lchar ')'

919− reservedOp "=>"

933+ reservedOp "=>"

920− return tys)

934+ return tys)

921− <|> try (do t <- expr (disallowImp syn)

935+ <|> try (do t <- expr (disallowImp syn)

922− reservedOp "=>"

936+ reservedOp "=>"

923− return [(defname, t)])

937+ return [(defname, t)])

924− <|> return []

925− <?> "type constraint list"

938+ <?> "type constraint list"

926 where nexpr = try (do n <- name; lchar ':'

939 where nexpr = try (do n <- name; lchar ':'

927 e <- expr' (disallowImp syn)

940 e <- expr' (disallowImp syn)

928 return (n, e))

941 return (n, e))

src/Idris/PartialEval.hs+12−12

@@ -85,35 +85,35 @@ specType args ty = let (t, args') = runState (unifyEq args ty) [] in

85 where

86 -- Specialise static argument in type by let-binding provided value instead

87 -- 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)

89 = 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)

91 = Bind n (Let t v) (st xs sc)

92 -- Erase argument from function type

93− st ((UnifiedD, _) : xs) (Bind n (Pi t _) sc)

93+ st ((UnifiedD, _) : xs) (Bind n (Pi _ t _) sc)

94 = st xs sc

95 -- Keep types as is

96− st (_ : xs) (Bind n (Pi t k) sc)

96+ st (_ : xs) (Bind n (Pi i t k) sc)

97− = Bind n (Pi t k) (st xs sc)

97+ = Bind n (Pi i t k) (st xs sc)

98 st _ t = t

99

100 -- Erase implicit dynamic argument if existing argument shares it value,

101 -- 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)

103 = do amap <- get

104 case lookup imp amap of

105 Just n' ->

106 do put (amap ++ [((UnifiedD, Erased), n)])

107 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

109 _ -> do put (amap ++ [(imp, n)])

110 sc' <- unifyEq xs sc

111− return (Bind n (Pi t k) sc')

111+ return (Bind n (Pi i t k) sc')

112− unifyEq (x : xs) (Bind n (Pi t k) sc)

112+ unifyEq (x : xs) (Bind n (Pi i t k) sc)

113 = do args <- get

114 put (args ++ [(x, n)])

115 sc' <- unifyEq xs sc

116− return (Bind n (Pi t k) sc')

116+ return (Bind n (Pi i t k) sc')

117 unifyEq xs t = do args <- get

118 put (args ++ (zip xs (repeat (sUN "_"))))

119 return t

@@ -127,9 +127,9 @@ specType args ty = let (t, args') = runState (unifyEq args ty) [] in

127mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Type -> PTerm

128mkPE_TyDecl ist args ty = mkty args ty

129 where

130− mkty ((ExplicitD, v) : xs) (Bind n (Pi t k) sc)

130+ mkty ((ExplicitD, v) : xs) (Bind n (Pi _ t k) sc)

131 = 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)

133 | concreteClass ist t = mkty xs sc

134 | classConstraint ist t

135 = 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,

26

27ty :: [Const] -> Const -> Type

28ty [] 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)

30

31total, partial, iopartial :: Totality

32total = Total []

src/Idris/REPL.hs+1−1

@@ -402,7 +402,7 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.Metavariables cols) =

402 -- | Split a function type into a pair of premises, conclusion.

403 -- Each maintains both the original and delaborated versions.

404 splitPi :: IState -> Type -> ([(Name, Type, PTerm)], Type, PTerm)

405− splitPi ist (Bind n (Pi t _) rest) =

405+ splitPi ist (Bind n (Pi _ t _) rest) =

406 let (hs, c, pc) = splitPi ist rest in

407 ((n, t, delabTy' ist [] t False False):hs,

408 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 ,

120 (arguments, theRemovedArgs, retTy) = go [] [] t

121

122 -- 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

124 if removePred ty

125 then go args (arg : removedArgs) sc

126 else go (arg : args) removedArgs sc

@@ -416,7 +416,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

416 unifyQueue state [] = return state

417 unifyQueue state ((ty1, ty2) : queue) = do

418 --trace ("go: \n" ++ show state) True `seq` return ()

419− res <- tcToMaybe $ match_unify ctxt [ (n, Pi ty (TType (UVar 0))) | (n, ty) <- holes state] ty1 ty2 [] (map fst $ holes state) []

419+ res <- tcToMaybe $ match_unify ctxt [ (n, Pi Nothing ty (TType (UVar 0))) | (n, ty) <- holes state] ty1 ty2 [] (map fst $ holes state) []

420 (state', queueAdditions) <- resolveUnis res state

421 guard $ scoreCriterion (score state')

422 unifyQueue state' (queue ++ queueAdditions)

test/basic012/basic012.idrnew file+62

@@ -0,0 +1,62 @@

1+import Data.Vect

2+import Control.Monad.State

3+import Control.Monad.Identity

4+

5+VThing : Type

6+VThing = {n : Nat} -> Vect n Int -> Int

7+

8+foo : Int -> Vect m Int -> ({n : Nat} -> Vect n Int -> Int) -> Int

9+foo x xs f = x + f xs

10+

11+foo' : Int -> Vect m Int -> VThing -> Int

12+foo' x xs f = x + f xs

13+

14+bar : Int -> VThing

15+bar y [] = 0

16+bar y (x :: xs) = y + x + bar y xs

17+

18+vsum : Vect n Int -> Int

19+vsum [] = 0

20+vsum (x :: xs) = x + vsum xs

21+

22+testfoo : Vect n Int -> Int

23+testfoo xs = foo 42 xs (\ xs => vsum xs)

24+

25+testfoo2 : Vect n Int -> Int

26+testfoo2 xs = foo' 42 xs vsum

27+

28+testfoo3 : Vect n Int -> Int

29+testfoo3 xs = foo 42 xs (bar 10)

30+

31+AnyST : Type -> Type -> Type

32+AnyST s a = {m : _} -> Monad m => StateT s m a

33+

34+foost: AnyST Int ()

35+foost = do x <- get

36+ put x

37+

38+wibble : StateT Int Maybe ()

39+wibble = foost

40+

41+appShow : Show a => ({b : _} -> Show b => b -> String) -> a -> String

42+appShow s x = s x

43+

44+myshow : Show a => a -> String

45+myshow = show

46+

47+baz : Int -> String

48+baz x = appShow myshow x ++ appShow show x

49+

50+tupleId : ({a : _} -> a -> a) -> (a, b) -> (a, b)

51+tupleId f (a, b) = (f a, f b)

52+

53+AppendType : Type

54+AppendType = {a, n, m : _} -> Vect n a -> Vect m a -> Vect (n + m) a

55+

56+append : AppendType

57+append [] ys = ys

58+append (x :: xs) ys = x :: append xs ys

59+

60+main : IO ()

61+main = do putStrLn (baz 42)

62+ print (append [1,2,3] [4,5,6])

test/basic012/expectednew file+2

@@ -0,0 +1,2 @@

1+4242

2+[1, 2, 3, 4, 5, 6]

test/basic012/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ basic012.idr -o basic012

3+./basic012

4+rm -f basic012 *.ibc

test/proof007/expected+1−1

@@ -1,3 +1,3 @@

1−DefaultArgUnknownName.idr:5:30:When elaborating right hand side of test:

1+DefaultArgUnknownName.idr:9:6:When elaborating right hand side of test:

2When elaborating argument [95marg[0m to function [92mDefaultArgUnknownName.funWithBadDefArg[0m:

3 No such variable sadgjhsag