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

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

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

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

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."

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

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

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

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

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

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
 

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

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)
+hasEmptyPat defs env (Bind fc x b sc)
-   = pure $ !(isEmpty defs env !(nf defs env ty))
+   = pure $ !(isEmpty defs env !(nf defs env (binderType b)))
             || !(hasEmptyPat defs (b :: env) sc)
 hasEmptyPat defs env _ = pure False
 

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

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

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

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 | 

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!

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!

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!

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!

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
 

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

tests/idris2/reg041/tuple.idr

@@ -1,5 +1,5 @@
 tupleBug : Pair () a -> ()
-tupleBug (_, _, _) = ()
+tupleBug (_, (_, _)) = ()
 
 odd : a -> Bool
 odd () = False

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: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:21}_[] ?Main.{b:19}_[])
+	Vect3:25:9--25:11:Type mismatch: Main.Nat and (Main.Vect ?Main.{n:22}_[] ?Main.{b:20}_[])
 Yaffle> Bye for now!

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!

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!

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!