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!

Author: edwinb

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,20 +437,34 @@ 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
              -- If we're on the LHS, reinstantiate it with 'argv' because it
              -- *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