From 97ee3d4cd3784103c32990fd6bf5bbb98a76a9c1 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sun, 13 Jun 2021 13:31:40 +0100 Subject: [PATCH] Check LHS arguments are polymorphic enough We already did this, but missed a few cases due to the way arguments are elaborated. So now, when checking an LHS, we don't allow LHS argument types to be inferred from the pattern, but rather they must be inferred from elsewhere. To do this, we keep track of the constraints which would be solved when inferring the type, and make sure they don't solve any new metavariables. Fixes #1510, and also now gets the error location right as a bonus! --- src/Core/Coverage.idr | 1 - src/Core/Unify.idr | 9 ++++- src/Core/UnifyState.idr | 45 +++++++++++++++++++++++ src/Idris/Error.idr | 2 +- src/TTImp/Elab.idr | 1 + src/TTImp/Elab/Ambiguity.idr | 4 +-- src/TTImp/Elab/App.idr | 51 +++++++++++--------------- src/TTImp/Elab/Check.idr | 29 +++++++++++++++ src/TTImp/Elab/Delayed.idr | 23 ++++++++++-- src/TTImp/Elab/ImplicitBind.idr | 53 +++++++++++++++++++++++++--- src/TTImp/Elab/Term.idr | 15 +++++++- src/TTImp/ProcessDef.idr | 4 +-- tests/Main.idr | 2 +- tests/idris2/coverage003/expected | 6 ++-- tests/idris2/coverage004/expected | 6 ++-- tests/idris2/error018/expected | 2 +- tests/idris2/interactive002/expected | 2 +- tests/idris2/literate001/expected | 2 +- tests/idris2/literate012/expected | 2 +- tests/idris2/literate016/expected | 2 +- tests/idris2/real002/Control/App.idr | 2 +- tests/idris2/reg041/expected | 16 ++++----- tests/idris2/reg041/tuple.idr | 2 +- tests/ttimp/coverage001/expected | 6 ++-- tests/ttimp/coverage002/expected | 2 +- tests/ttimp/eta001/expected | 2 +- tests/ttimp/eta002/expected | 2 +- 27 files changed, 220 insertions(+), 73 deletions(-) diff --git a/src/Core/Coverage.idr b/src/Core/Coverage.idr index c8f9705ce..b55ea2a59 100644 --- a/src/Core/Coverage.idr +++ b/src/Core/Coverage.idr @@ -141,7 +141,6 @@ isEmpty : {vars : _} -> isEmpty defs env (NTCon fc n t a args) = do Just nty <- lookupDefExact n (gamma defs) | _ => pure False - log "coverage.empty" 10 $ "Checking type: " ++ show nty case nty of TCon _ _ _ _ flags _ cons _ => if not (external flags) diff --git a/src/Core/Unify.idr b/src/Core/Unify.idr index 64a1b4ea0..0d57d1f0b 100644 --- a/src/Core/Unify.idr +++ b/src/Core/Unify.idr @@ -831,10 +831,11 @@ mutual Core UnifyResult solveHole loc mode env mname mref margs margs' locs submv solfull stm solnf = do defs <- get Ctxt + ust <- get UST empty <- clearDefs defs -- if the terms are the same, this isn't a solution -- but they are already unifying, so just return - if solutionHeadSame solnf + if solutionHeadSame solnf || inNoSolve mref (noSolve ust) then pure success else -- Rather than doing the occurs check here immediately, -- we'll wait until all metavariables are resolved, and in @@ -846,6 +847,12 @@ mutual instantiate loc mode env mname mref (length margs) hdef locs solfull stm pure $ solvedHole mref where + inNoSolve : Int -> IntMap () -> Bool + inNoSolve i ns + = case lookup i ns of + Nothing => False + Just _ => True + -- Only need to check the head metavar is the same, we've already -- checked the rest if they are the same (and we couldn't instantiate it -- anyway...) diff --git a/src/Core/UnifyState.idr b/src/Core/UnifyState.idr index 2682aac7e..1eaa9d013 100644 --- a/src/Core/UnifyState.idr +++ b/src/Core/UnifyState.idr @@ -43,6 +43,18 @@ data Constraint : Type where -- A resolved constraint Resolved : Constraint +-- a constraint on the LHS arising from checking an argument in a position +-- where we expect a polymorphic type. If, in the end, the expected type is +-- polymorphic but the argument is concrete, then the pattern match is too +-- specific +public export +data PolyConstraint : Type where + MkPolyConstraint : {vars : _} -> + FC -> Env Term vars -> + (arg : Term vars) -> + (expty : NF vars) -> + (argty : NF vars) -> PolyConstraint + public export record UState where constructor MkUState @@ -57,6 +69,12 @@ record UState where -- user defined hole names, which don't need -- to have been solved constraints : IntMap Constraint -- map for finding constraints by ID + noSolve : IntMap () -- Names not to solve + -- If we're checking an LHS, then checking an argument can't + -- solve its own type, or we might end up with something + -- less polymorphic than it should be + polyConstraints : List PolyConstraint -- constraints which need to be solved + -- successfully to check an LHS is polymorphic enough dotConstraints : List (Name, DotReason, Constraint) -- dot pattern constraints nextName : Int nextConstraint : Int @@ -77,6 +95,8 @@ initUState = MkUState , currentHoles = empty , delayedHoles = empty , constraints = empty + , noSolve = empty + , polyConstraints = [] , dotConstraints = [] , nextName = 0 , nextConstraint = 0 @@ -180,6 +200,20 @@ removeHoleName n | Nothing => pure () removeHole i +export +addNoSolve : {auto u : Ref UST UState} -> + Int -> Core () +addNoSolve i + = do ust <- get UST + put UST (record { noSolve $= insert i () } ust) + +export +removeNoSolve : {auto u : Ref UST UState} -> + Int -> Core () +removeNoSolve i + = do ust <- get UST + put UST (record { noSolve $= delete i } ust) + export saveHoles : {auto u : Ref UST UState} -> Core (IntMap (FC, Name)) @@ -281,6 +315,17 @@ addDot fc env dotarg x reason y ((dotarg, reason, MkConstraint fc False env xnf ynf) ::) } ust) +export +addPolyConstraint : {vars : _} -> + {auto u : Ref UST UState} -> + FC -> Env Term vars -> Term vars -> NF vars -> NF vars -> + Core () +addPolyConstraint fc env arg x@(NApp _ (NMeta _ _ _) _) y + = do ust <- get UST + put UST (record { polyConstraints $= ((MkPolyConstraint fc env arg x y) ::) } ust) +addPolyConstraint fc env arg x y + = pure () + mkConstantAppArgs : {vars : _} -> Bool -> FC -> Env Term vars -> (wkns : List Name) -> diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index 79f619769..cc276a0d1 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -428,7 +428,7 @@ perror (BadDotPattern fc env reason x y) <++> parens (pretty reason) <+> dot) <+> line <+> !(ploc fc) perror (MatchTooSpecific fc env tm) = pure $ errorDesc (reflow "Can't match on" <++> code !(pshow env tm) - <++> reflow "as it has a polymorphic type.") <+> line <+> !(ploc fc) + <++> reflow "as it must have a polymorphic type.") <+> line <+> !(ploc fc) perror (BadImplicit fc str) = pure $ errorDesc (reflow "Can't infer type for unbound implicit name" <++> code (pretty str) <+> dot) <+> line <+> !(ploc fc) <+> line <+> reflow "Suggestion: try making it a bound implicit." diff --git a/src/TTImp/Elab.idr b/src/TTImp/Elab.idr index f8e0585fc..534ab75cb 100644 --- a/src/TTImp/Elab.idr +++ b/src/TTImp/Elab.idr @@ -9,6 +9,7 @@ import Core.Metadata import Core.Normalise import Core.UnifyState import Core.Unify +import Core.Value import TTImp.Elab.Check import TTImp.Elab.Delayed diff --git a/src/TTImp/Elab/Ambiguity.idr b/src/TTImp/Elab/Ambiguity.idr index d7461c789..86e3001d3 100644 --- a/src/TTImp/Elab/Ambiguity.idr +++ b/src/TTImp/Elab/Ambiguity.idr @@ -383,7 +383,7 @@ checkAlternative rig elabinfo nest env fc (UniqueDefault def) alts mexpected checkImp rig (addAmbig alts' (getName t) elabinfo) nest env t (Just exp'))) alts')) - (do log "elab" 5 "All failed, running default" + (do log "elab.ambiguous" 5 "All failed, running default" checkImp rig (addAmbig alts' (getName def) elabinfo) nest env def (Just exp')) else exactlyOne' True fc env @@ -441,5 +441,5 @@ checkAlternative rig elabinfo nest env fc uniq alts mexpected -- way that allows one pass) solveConstraints solvemode Normal solveConstraints solvemode Normal - log "elab" 10 $ show (getName t) ++ " success" + log "elab.ambiguous" 10 $ show (getName t) ++ " success" pure res)) alts') diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr index 06643bfec..89d0881f6 100644 --- a/src/TTImp/Elab/App.idr +++ b/src/TTImp/Elab/App.idr @@ -153,18 +153,6 @@ isHole : NF vars -> Bool isHole (NApp _ (NMeta _ _ _) _) = True isHole _ = False --- Return whether we already know the return type of the given function --- type. If we know this, we can possibly infer some argument types before --- elaborating them, which might help us disambiguate things more easily. -concrete : Defs -> Env Term vars -> NF vars -> Core Bool -concrete defs env (NBind fc _ (Pi _ _ _ _) sc) - = do sc' <- sc defs (toClosure defaultOpts env (Erased fc False)) - concrete defs env sc' -concrete defs env (NDCon _ _ _ _ _) = pure True -concrete defs env (NTCon _ _ _ _ _) = pure True -concrete defs env (NPrimVal _ _) = pure True -concrete defs env _ = pure False - mutual makeImplicit : {vars : _} -> {auto c : Ref Ctxt Defs} -> @@ -324,9 +312,11 @@ mutual needsDelayLHS (IAutoApp _ f _) = needsDelayLHS f needsDelayLHS (INamedApp _ f _ _) = needsDelayLHS f needsDelayLHS (IAlternative _ _ _) = pure True + needsDelayLHS (IAs _ _ _ _ t) = needsDelayLHS t needsDelayLHS (ISearch _ _) = pure True needsDelayLHS (IPrimVal _ _) = pure True needsDelayLHS (IType _) = pure True + needsDelayLHS (IWithUnambigNames _ _ t) = needsDelayLHS t needsDelayLHS _ = pure False onLHS : ElabMode -> Bool @@ -355,21 +345,6 @@ mutual Bind _ _ (Lam _ _ _ _) _ => registerDot rig env fc NotConstructor tm ty _ => pure (tm, ty) - - checkPatTyValid : {vars : _} -> - {auto c : Ref Ctxt Defs} -> - FC -> Defs -> Env Term vars -> - NF vars -> Term vars -> Glued vars -> Core () - checkPatTyValid fc defs env (NApp _ (NMeta n i _) _) arg got - = do Just gdef <- lookupCtxtExact (Resolved i) (gamma defs) - | Nothing => pure () - when (isErased (multiplicity gdef)) $ do - -- Argument is only valid if gotnf is not a concrete type - gotnf <- getNF got - when !(concrete defs env gotnf) $ - throw (MatchTooSpecific fc env arg) - checkPatTyValid fc defs env _ _ _ = pure () - dotErased : {auto c : Ref Ctxt Defs} -> (argty : NF vars) -> Maybe Name -> Nat -> ElabMode -> RigCount -> RawImp -> Core RawImp dotErased argty mn argpos (InLHS lrig ) rig tm @@ -462,12 +437,26 @@ mutual aty' <- nf defs env metaty logNF "elab" 10 ("Now trying " ++ show nm ++ " " ++ show arg) env aty' - res <- check argRig elabinfo nest env arg (Just $ glueBack defs env aty') + -- On the LHS, checking an argument can't resolve its own type, + -- it must be resolved from elsewhere. Otherwise we might match + -- on things which are too specific for their polymorphic type. + when (onLHS (elabMode elabinfo)) $ + case aty' of + NApp _ (NMeta _ i _) _ => + do Just gdef <- lookupCtxtExact (Resolved i) (gamma defs) + | Nothing => pure () + when (isErased (multiplicity gdef)) $ addNoSolve i + _ => pure () + res <- check argRig (record { topLevel = False } elabinfo) nest env arg (Just $ glueBack defs env aty') + when (onLHS (elabMode elabinfo)) $ + case aty' of + NApp _ (NMeta _ i _) _ => removeNoSolve i + _ => pure () + (argv, argt) <- if not (onLHS (elabMode elabinfo)) then pure res else do let (argv, argt) = res - checkPatTyValid fc defs env aty' argv argt checkValidPattern rig env fc argv argt defs <- get Ctxt @@ -475,7 +464,7 @@ mutual -- *may* have as patterns in it and we need to retain them. -- (As patterns are a bit of a hack but I don't yet see a -- better way that leads to good code...) - logTerm "elab" 5 ("Solving " ++ show metaval ++ " with") argv + logTerm "elab" 10 ("Solving " ++ show metaval ++ " with") argv ok <- solveIfUndefined env metaval argv -- If there's a constraint, make a constant, but otherwise -- just return the term as expected @@ -503,7 +492,7 @@ mutual (\t => pure (Just !(toFullNames!(getTerm t)))) expty pure ("Overall expected type: " ++ show ety)) - res <- check argRig elabinfo + res <- check argRig (record { topLevel = False } elabinfo) nest env arg (Just (glueBack defs env aty)) (argv, argt) <- if not (onLHS (elabMode elabinfo)) diff --git a/src/TTImp/Elab/Check.idr b/src/TTImp/Elab/Check.idr index 368a40fab..4590b9a52 100644 --- a/src/TTImp/Elab/Check.idr +++ b/src/TTImp/Elab/Check.idr @@ -135,6 +135,10 @@ record EState (vars : List Name) where allPatVars : List Name -- Holes standing for pattern variables, which we'll delete -- once we're done elaborating + polyMetavars : List (FC, Env Term vars, Term vars, Term vars) + -- Metavars which need to be a polymorphic type at the end + -- of elaboration. If they aren't, it means we're trying to + -- pattern match on a type that we don't have available. delayDepth : Nat -- if it gets too deep, it gets slow, so fail quicker linearUsed : List (Var vars) saveHoles : NameMap () -- things we'll need to save to TTC, even if solved @@ -159,6 +163,7 @@ initEStateSub n env sub = MkEState , bindIfUnsolved = [] , lhsPatVars = [] , allPatVars = [] + , polyMetavars = [] , delayDepth = Z , linearUsed = [] , saveHoles = empty @@ -187,6 +192,7 @@ weakenedEState {e} , boundNames $= map wknTms , toBind $= map wknTms , linearUsed $= map weaken + , polyMetavars = [] -- no binders on LHS } est pure eref where @@ -212,6 +218,7 @@ strengthenedEState {n} {vars} c e fc env , boundNames = bns , toBind = todo , linearUsed $= mapMaybe dropTop + , polyMetavars = [] -- no binders on LHS } est where @@ -287,6 +294,28 @@ inScope {c} {e} fc env elab put {ref=e} EST st' pure res +export +mustBePoly : {auto e : Ref EST (EState vars)} -> + FC -> Env Term vars -> + Term vars -> Term vars -> Core () +mustBePoly fc env tm ty + = do est <- get EST + put EST (record { polyMetavars $= ((fc, env, tm, ty) :: ) } est) + +-- Return whether we already know the return type of the given function +-- type. If we know this, we can possibly infer some argument types before +-- elaborating them, which might help us disambiguate things more easily. +export +concrete : Defs -> Env Term vars -> NF vars -> Core Bool +concrete defs env (NBind fc _ (Pi _ _ _ _) sc) + = do sc' <- sc defs (toClosure defaultOpts env (Erased fc False)) + concrete defs env sc' +concrete defs env (NDCon _ _ _ _ _) = pure True +concrete defs env (NTCon _ _ _ _ _) = pure True +concrete defs env (NPrimVal _ _) = pure True +concrete defs env (NType _) = pure True +concrete defs env _ = pure False + export updateEnv : {new : _} -> Env Term new -> SubVars new vars -> diff --git a/src/TTImp/Elab/Delayed.idr b/src/TTImp/Elab/Delayed.idr index 261ca2038..7fafcf3da 100644 --- a/src/TTImp/Elab/Delayed.idr +++ b/src/TTImp/Elab/Delayed.idr @@ -70,6 +70,8 @@ delayOnFailure : {vars : _} -> Core (Term vars, Glued vars) delayOnFailure fc rig env expected pred pri elab = do est <- get EST + ust <- get UST + let nos = noSolve ust -- remember the holes we shouldn't solve handle (elab False) (\err => do est <- get EST @@ -85,7 +87,15 @@ delayOnFailure fc rig env expected pred pri elab defs <- get Ctxt put UST (record { delayedElab $= ((pri, ci, localHints defs, - mkClosedElab fc env (deeper (elab True))) :: ) } + mkClosedElab fc env + (deeper + (do ust <- get UST + let nos' = noSolve ust + put UST (record { noSolve = nos } ust) + res <- elab True + ust <- get UST + put UST (record { noSolve = nos' } ust) + pure res))) :: ) } ust) pure (dtm, expected) else throw err) @@ -103,6 +113,8 @@ delayElab : {vars : _} -> Core (Term vars, Glued vars) delayElab {vars} fc rig env exp pri elab = do est <- get EST + ust <- get UST + let nos = noSolve ust -- remember the holes we shouldn't solve nm <- genName "delayed" expected <- mkExpected exp (ci, dtm) <- newDelayed fc linear env nm !(getTerm expected) @@ -111,7 +123,14 @@ delayElab {vars} fc rig env exp pri elab ust <- get UST defs <- get Ctxt put UST (record { delayedElab $= - ((pri, ci, localHints defs, mkClosedElab fc env elab) :: ) } + ((pri, ci, localHints defs, mkClosedElab fc env + (do ust <- get UST + let nos' = noSolve ust + put UST (record { noSolve = nos } ust) + res <- elab + ust <- get UST + put UST (record { noSolve = nos' } ust) + pure res)) :: ) } ust) pure (dtm, expected) where diff --git a/src/TTImp/Elab/ImplicitBind.idr b/src/TTImp/Elab/ImplicitBind.idr index 9080fe965..56dba4eb7 100644 --- a/src/TTImp/Elab/ImplicitBind.idr +++ b/src/TTImp/Elab/ImplicitBind.idr @@ -9,6 +9,7 @@ import Core.Env import Core.Metadata import Core.Normalise import Core.Unify +import Core.UnifyState import Core.TT import Core.Value @@ -473,6 +474,40 @@ checkBindVar rig elabinfo nest env fc str topexp combine n l r = when (isIncompatible l r) (throw (LinearUsed fc 2 n)) +checkPolyConstraint : + {auto c : Ref Ctxt Defs} -> + PolyConstraint -> Core () +checkPolyConstraint (MkPolyConstraint fc env arg x y) + = do defs <- get Ctxt + -- If 'x' is a metavariable and 'y' is concrete, that means we've + -- ended up putting something too concrete in for a polymorphic + -- argument + xnf <- continueNF defs env x + case xnf of + NApp _ (NMeta _ _ _) _ => + do ynf <- continueNF defs env y + if !(concrete defs env ynf) + then do empty <- clearDefs defs + throw (MatchTooSpecific fc env arg) + else pure () + _ => pure () +checkPolyConstraint _ = pure () + +solvePolyConstraint : + {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + PolyConstraint -> Core () +solvePolyConstraint (MkPolyConstraint fc env arg x y) + = do defs <- get Ctxt + -- If the LHS of the constraint isn't a metavariable, we can solve + -- the constraint + case !(continueNF defs env x) of + xnf@(NApp _ (NMeta _ _ _) _) => pure () + t => do res <- unify inLHS fc env t !(continueNF defs env y) + -- If there's any constraints, it just means we didn't + -- solve anything and it won't help the check + pure () + export checkBindHere : {vars : _} -> {auto c : Ref Ctxt Defs} -> @@ -501,16 +536,26 @@ checkBindHere rig elabinfo nest env fc bindmode tm exp solveConstraints (case elabMode elabinfo of InLHS c => inLHS _ => inTerm) Normal - solveConstraintsAfter constart - (case elabMode elabinfo of - InLHS c => inLHS - _ => inTerm) Defaults + ust <- get UST catch (retryDelayed (delayedElab ust)) (\err => do ust <- get UST put UST (record { delayedElab = [] } ust) throw err) + + -- Check all the patterns standing for polymorphic variables are + -- indeed polymorphic + ust <- get UST + let cons = polyConstraints ust + put UST (record { polyConstraints = [] } ust) + traverse_ solvePolyConstraint cons + traverse_ checkPolyConstraint cons + + solveConstraintsAfter constart + (case elabMode elabinfo of + InLHS c => inLHS + _ => inTerm) Defaults checkDots -- Check dot patterns unifying with the claimed thing -- before binding names diff --git a/src/TTImp/Elab/Term.idr b/src/TTImp/Elab/Term.idr index 5edea7d53..e5529d8b8 100644 --- a/src/TTImp/Elab/Term.idr +++ b/src/TTImp/Elab/Term.idr @@ -295,6 +295,10 @@ TTImp.Elab.Check.check rigc elabinfo nest env tm_in exp _ => do tm' <- insertImpLam env tm exp checkImp rigc elabinfo nest env tm' exp +onLHS : ElabMode -> Bool +onLHS (InLHS _) = True +onLHS _ = False + -- As above, but doesn't add any implicit lambdas, forces, delays, etc -- checkImp : {vars : _} -> -- {auto c : Ref Ctxt Defs} -> @@ -304,4 +308,13 @@ TTImp.Elab.Check.check rigc elabinfo nest env tm_in exp -- RigCount -> ElabInfo -> Env Term vars -> RawImp -> Maybe (Glued vars) -> -- Core (Term vars, Glued vars) TTImp.Elab.Check.checkImp rigc elabinfo nest env tm exp - = checkTerm rigc elabinfo nest env tm exp + = do res <- checkTerm rigc elabinfo nest env tm exp + -- LHS arguments can't infer their own type - they need to be inferred + -- from some other argument. This is to prevent arguments being not + -- polymorphic enough. So, here, add the constraint to be checked later. + when (onLHS (elabMode elabinfo) && not (topLevel elabinfo)) $ + do let (argv, argt) = res + let Just expty = exp + | Nothing => pure () + addPolyConstraint (getFC tm) env argv !(getNF expty) !(getNF argt) + pure res diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr index 1aa7307d5..3a89b7e76 100644 --- a/src/TTImp/ProcessDef.idr +++ b/src/TTImp/ProcessDef.idr @@ -386,8 +386,8 @@ checkLHS {vars} trans mult hashit n opts nest env fc lhs_in hasEmptyPat : {vars : _} -> {auto c : Ref Ctxt Defs} -> Defs -> Env Term vars -> Term vars -> Core Bool -hasEmptyPat defs env (Bind fc x b@(PVar _ _ _ ty) sc) - = pure $ !(isEmpty defs env !(nf defs env ty)) +hasEmptyPat defs env (Bind fc x b sc) + = pure $ !(isEmpty defs env !(nf defs env (binderType b))) || !(hasEmptyPat defs (b :: env) sc) hasEmptyPat defs env _ = pure False diff --git a/tests/Main.idr b/tests/Main.idr index 28d121412..0a15b029d 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -122,7 +122,7 @@ idrisTestsRegression = MkTestPool "Various regressions" [] "reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021", "reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028", "reg029", "reg030", "reg031", "reg032", "reg033", "reg034", "reg035", - "reg036", "reg037", "reg038", "reg039", "reg040"] + "reg036", "reg037", "reg038", "reg039", "reg040", "reg041"] idrisTestsData : TestPool idrisTestsData = MkTestPool "Data and record types" [] diff --git a/tests/idris2/coverage003/expected b/tests/idris2/coverage003/expected index d36bc3d45..90bf0d485 100644 --- a/tests/idris2/coverage003/expected +++ b/tests/idris2/coverage003/expected @@ -1,13 +1,13 @@ 1/1: Building Cover (Cover.idr) -Error: While processing left hand side of badBar. Can't match on 0 as it has a polymorphic type. +Error: While processing left hand side of badBar. Can't match on 0 as it must have a polymorphic type. -Cover:16:1--16:7 +Cover:16:8--16:9 12 | cty Nat (S _) = S Z 13 | cty _ x = S (S Z) 14 | 15 | badBar : a -> Nat 16 | badBar Z = Z - ^^^^^^ + ^ Main> Main.foo: foo (0, S _) foo (S _, _) diff --git a/tests/idris2/coverage004/expected b/tests/idris2/coverage004/expected index 3fe6627aa..9493332a0 100644 --- a/tests/idris2/coverage004/expected +++ b/tests/idris2/coverage004/expected @@ -1,13 +1,13 @@ 1/1: Building Cover (Cover.idr) -Error: While processing left hand side of bad. Can't match on Just (fromInteger 0) as it has a polymorphic type. +Error: While processing left hand side of bad. Can't match on Just (fromInteger 0) as it must have a polymorphic type. -Cover:14:1--14:4 +Cover:14:6--14:12 10 | 11 | bad : a -> Foo a -> Bool 12 | bad Z IsNat = False 13 | bad True IsBool = True 14 | bad (Just 0) _ = False - ^^^ + ^^^^^^ Main> Main.okay: okay (S _) IsNat okay False IsBool diff --git a/tests/idris2/error018/expected b/tests/idris2/error018/expected index ece086490..227034f28 100644 --- a/tests/idris2/error018/expected +++ b/tests/idris2/error018/expected @@ -30,7 +30,7 @@ Issue1031-3:4:6--4:7 1/1: Building Issue1031-4 (Issue1031-4.idr) Error: While processing left hand side of nice. Unsolved holes: -Main.{dotTm:306} introduced at: +Main.{dotTm:335} introduced at: Issue1031-4:4:6--4:10 1 | %default total 2 | diff --git a/tests/idris2/interactive002/expected b/tests/idris2/interactive002/expected index b72087379..ca29c4c7e 100644 --- a/tests/idris2/interactive002/expected +++ b/tests/idris2/interactive002/expected @@ -4,5 +4,5 @@ append {n = (S k)} (x :: xs) ys = ?foo_2 Main> vadd [] [] = ?bar_1 Main> vadd (x :: xs) (y :: ys) = ?baz_1 Main> suc x x Refl = ?quux_1 -Main> suc' {x = y} {y = y} Refl = ?quuz_1 +Main> suc' {x = x} {y = x} Refl = ?quuz_1 Main> Bye for now! diff --git a/tests/idris2/literate001/expected b/tests/idris2/literate001/expected index 6f0fdf400..f1bf6bad2 100644 --- a/tests/idris2/literate001/expected +++ b/tests/idris2/literate001/expected @@ -4,5 +4,5 @@ Main> > append {n = 0} [] ys = ?foo_1 Main> > vadd [] [] = ?bar_1 Main> > vadd (x :: xs) (y :: ys) = ?baz_1 Main> > suc x x Refl = ?quux_1 -Main> > suc' {x = y} {y = y} Refl = ?quuz_1 +Main> > suc' {x = x} {y = x} Refl = ?quuz_1 Main> Bye for now! diff --git a/tests/idris2/literate012/expected b/tests/idris2/literate012/expected index 668aec99b..b8e39db2c 100644 --- a/tests/idris2/literate012/expected +++ b/tests/idris2/literate012/expected @@ -4,5 +4,5 @@ append {n = (S k)} (x :: xs) ys = ?foo_2 Main> vadd [] [] = ?bar_1 Main> vadd (x :: xs) (y :: ys) = ?baz_1 Main> suc x x Refl = ?quux_1 -Main> suc' {x = y} {y = y} Refl = ?quuz_1 +Main> suc' {x = x} {y = x} Refl = ?quuz_1 Main> Bye for now! diff --git a/tests/idris2/literate016/expected b/tests/idris2/literate016/expected index 668aec99b..b8e39db2c 100644 --- a/tests/idris2/literate016/expected +++ b/tests/idris2/literate016/expected @@ -4,5 +4,5 @@ append {n = (S k)} (x :: xs) ys = ?foo_2 Main> vadd [] [] = ?bar_1 Main> vadd (x :: xs) (y :: ys) = ?baz_1 Main> suc x x Refl = ?quux_1 -Main> suc' {x = y} {y = y} Refl = ?quuz_1 +Main> suc' {x = x} {y = x} Refl = ?quuz_1 Main> Bye for now! diff --git a/tests/idris2/real002/Control/App.idr b/tests/idris2/real002/Control/App.idr index 57e9a2fd8..6589105f2 100644 --- a/tests/idris2/real002/Control/App.idr +++ b/tests/idris2/real002/Control/App.idr @@ -207,7 +207,7 @@ namespace App1 export delay : {u : _} -> (1 k : App1 {u=u'} e b) -> - Cont1Type u a u' e b + Cont1Type u () u' e b delay {u = One} mb = \ () => mb delay {u = Any} mb = \ _ => mb diff --git a/tests/idris2/reg041/expected b/tests/idris2/reg041/expected index 37f2220d8..8bbacd097 100644 --- a/tests/idris2/reg041/expected +++ b/tests/idris2/reg041/expected @@ -1,18 +1,18 @@ 1/1: Building tuple (tuple.idr) -Error: While processing left hand side of tupleBug. Can't match on (?_, ?_) as it has a polymorphic type. +Error: While processing left hand side of tupleBug. Can't match on (?_, ?_) as it must have a polymorphic type. -tuple:2:11--2:13 +tuple:2:15--2:19 1 | tupleBug : Pair () a -> () - 2 | tupleBug (_, _, _) = () - ^^ + 2 | tupleBug (_, (_, _)) = () + ^^^^ -Error: While processing left hand side of odd. Can't match on () as it has a polymorphic type. +Error: While processing left hand side of odd. Can't match on () as it must have a polymorphic type. -tuple:5:1--5:4 +tuple:5:5--5:7 1 | tupleBug : Pair () a -> () - 2 | tupleBug (_, _, _) = () + 2 | tupleBug (_, (_, _)) = () 3 | 4 | odd : a -> Bool 5 | odd () = False - ^^^ + ^^ diff --git a/tests/idris2/reg041/tuple.idr b/tests/idris2/reg041/tuple.idr index fca33b234..7fe14dd93 100644 --- a/tests/idris2/reg041/tuple.idr +++ b/tests/idris2/reg041/tuple.idr @@ -1,5 +1,5 @@ tupleBug : Pair () a -> () -tupleBug (_, _, _) = () +tupleBug (_, (_, _)) = () odd : a -> Bool odd () = False diff --git a/tests/ttimp/coverage001/expected b/tests/ttimp/coverage001/expected index 9269adf48..12de2348f 100644 --- a/tests/ttimp/coverage001/expected +++ b/tests/ttimp/coverage001/expected @@ -2,10 +2,10 @@ Processing as TTImp Written TTC Yaffle> Bye for now! Processing as TTImp -Vect2:25:1--26:1:{pat 0 {b:27} : Type} => {pat 0 {a:26} : Type} => ($resolved379 {b:27}[1] {a:26}[0] $resolved361 ($resolved370 {a:26}[0]) ($resolved370 {b:27}[1])) is not a valid impossible pattern because it typechecks +Vect2:25:1--26:1:{pat 0 {b:28} : Type} => {pat 0 {a:27} : Type} => ($resolved380 {b:28}[1] {a:27}[0] $resolved361 ($resolved370 {a:27}[0]) ($resolved370 {b:28}[1])) is not a valid impossible pattern because it typechecks Yaffle> Bye for now! Processing as TTImp Vect3:25:1--26:1:Not a valid impossible pattern: - Vect3:25:9--25:11:When unifying: Main.Nat and (Main.Vect ?Main.{n:21}_[] ?Main.{b:19}_[]) - Vect3:25:9--25:11:Type mismatch: Main.Nat and (Main.Vect ?Main.{n:21}_[] ?Main.{b:19}_[]) + Vect3:25:9--25:11:When unifying: Main.Nat and (Main.Vect ?Main.{n:22}_[] ?Main.{b:20}_[]) + Vect3:25:9--25:11:Type mismatch: Main.Nat and (Main.Vect ?Main.{n:22}_[] ?Main.{b:20}_[]) Yaffle> Bye for now! diff --git a/tests/ttimp/coverage002/expected b/tests/ttimp/coverage002/expected index 80e8fe3cd..30c642be6 100644 --- a/tests/ttimp/coverage002/expected +++ b/tests/ttimp/coverage002/expected @@ -2,6 +2,6 @@ Processing as TTImp Written TTC Yaffle> Main.lookup: All cases covered Yaffle> Main.lookup': -($resolved408 [__] [__] ($resolved376 [__]) {_:59}) +($resolved409 [__] [__] ($resolved377 [__]) {_:60}) Yaffle> Main.lookup'': Calls non covering function Main.lookup' Yaffle> Bye for now! diff --git a/tests/ttimp/eta001/expected b/tests/ttimp/eta001/expected index 695ea2c03..8ed996336 100644 --- a/tests/ttimp/eta001/expected +++ b/tests/ttimp/eta001/expected @@ -1,5 +1,5 @@ Processing as TTImp Written TTC -Yaffle> ((Main.Refl [{b:9} = Main.Nat]) [x = (Main.S (Main.S (Main.S (Main.S Main.Z))))]) +Yaffle> ((Main.Refl [{a:11} = Main.Nat]) [x = (Main.S (Main.S (Main.S (Main.S Main.Z))))]) Yaffle> Main.etaGood1 : ((((Main.Eq [b = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) [a = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) Main.MkTest) (%lam RigW Explicit (Just x) Integer (%lam RigW Explicit (Just y) Integer ((Main.MkTest x) y)))) Yaffle> Bye for now! diff --git a/tests/ttimp/eta002/expected b/tests/ttimp/eta002/expected index d5cf34b63..3f44c518e 100644 --- a/tests/ttimp/eta002/expected +++ b/tests/ttimp/eta002/expected @@ -1,5 +1,5 @@ Processing as TTImp Eta:16:1--17:1:When elaborating right hand side of Main.etaBad: -Eta:16:10--17:1:When unifying: (Main.Eq ({arg:10} : Integer) -> ({arg:11} : Integer) -> Main.Test)) ({arg:10} : Integer) -> ({arg:11} : Integer) -> Main.Test)) \(x : Char) => \(y : ?Main.{_:14}_[x[0]]) => (Main.MkTest x[1] y[0]) \(x : Char) => \(y : ?Main.{_:14}_[x[0]]) => (Main.MkTest x[1] y[0])) and (Main.Eq (x : Char) -> (y : ?Main.{_:14}_[x[0]]) -> Main.Test)) ({arg:10} : Integer) -> ({arg:11} : Integer) -> Main.Test)) Main.MkTest \(x : Char) => \(y : ?Main.{_:14}_[x[0]]) => (Main.MkTest x[1] y[0])) +Eta:16:10--17:1:When unifying: (Main.Eq ({arg:12} : Integer) -> ({arg:13} : Integer) -> Main.Test)) ({arg:12} : Integer) -> ({arg:13} : Integer) -> Main.Test)) \(x : Char) => \(y : ?Main.{_:18}_[x[0]]) => (Main.MkTest x[1] y[0]) \(x : Char) => \(y : ?Main.{_:18}_[x[0]]) => (Main.MkTest x[1] y[0])) and (Main.Eq (x : Char) -> (y : ?Main.{_:18}_[x[0]]) -> Main.Test)) ({arg:12} : Integer) -> ({arg:13} : Integer) -> Main.Test)) Main.MkTest \(x : Char) => \(y : ?Main.{_:18}_[x[0]]) => (Main.MkTest x[1] y[0])) Eta:16:10--17:1:Type mismatch: Integer and Char Yaffle> Bye for now!