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!