
    0 | module Core.Unify
    1 | 
    2 | import Core.Case.CaseTree
    3 | import Core.Context.Log
    4 | import Core.Env
    5 | import Core.GetType
    6 | import Core.Normalise
    7 | import Core.Options
    8 | import public Core.UnifyState
    9 | import Core.Value
   10 | 
   11 | import Data.Maybe
   12 | 
   13 | import Libraries.Data.List.SizeOf
   14 | 
   15 | import Libraries.Data.VarSet
   16 | 
   17 | import Libraries.Data.IntMap
   18 | import Libraries.Data.NameMap
   19 | 
   20 | %default covering
   21 | 
   22 | public export
   23 | data UnifyMode = InLHS
   24 |                | InTerm
   25 |                | InMatch
   26 |                | InSearch
   27 | 
   28 | -- Need to record if we're at the top level or not, because top level things
   29 | -- can have Force and Delay inserted, and may have been postponed.
   30 | public export
   31 | record UnifyInfo where
   32 |   constructor MkUnifyInfo
   33 |   atTop : Bool
   34 |   umode : UnifyMode
   35 | 
   36 | export
   37 | inTerm : UnifyInfo
   38 | inTerm = MkUnifyInfo True InTerm
   39 | 
   40 | export
   41 | inLHS : UnifyInfo
   42 | inLHS = MkUnifyInfo True InLHS
   43 | 
   44 | export
   45 | inMatch : UnifyInfo
   46 | inMatch = MkUnifyInfo True InMatch
   47 | 
   48 | export
   49 | inSearch : UnifyInfo
   50 | inSearch = MkUnifyInfo True InSearch
   51 | 
   52 | lower : UnifyInfo -> UnifyInfo
   53 | lower = { atTop := False }
   54 | 
   55 | Eq UnifyMode where
   56 |    InLHS == InLHS = True
   57 |    InTerm == InTerm = True
   58 |    InMatch == InMatch = True
   59 |    InSearch == InSearch = True
   60 |    _ == _ = False
   61 | 
   62 | Eq UnifyInfo where
   63 |   x == y = atTop x == atTop y && umode x == umode y
   64 | 
   65 | Show UnifyMode where
   66 |   show InLHS = "InLHS"
   67 |   show InTerm = "InTerm"
   68 |   show InMatch = "InMatch"
   69 |   show InSearch = "InSearch"
   70 | 
   71 | -- If we're unifying a Lazy type with a non-lazy type, we need to add an
   72 | -- explicit force or delay to the first argument to unification. This says
   73 | -- which to add, if any. Can only added at the very top level.
   74 | public export
   75 | data AddLazy = NoLazy | AddForce LazyReason | AddDelay LazyReason
   76 | 
   77 | export
   78 | Show AddLazy where
   79 |   show NoLazy = "NoLazy"
   80 |   show (AddForce _) = "AddForce"
   81 |   show (AddDelay _) = "AddDelay"
   82 | 
   83 | public export
   84 | record UnifyResult where
   85 |   constructor MkUnifyResult
   86 |   constraints : List Int
   87 |   holesSolved : Bool -- did we solve any holes
   88 |   namesSolved : List Int -- which ones did we solve (as name indices)
   89 |   addLazy : AddLazy
   90 | 
   91 | union : UnifyResult -> UnifyResult -> UnifyResult
   92 | union u1 u2 = MkUnifyResult (union (constraints u1) (constraints u2))
   93 |                             (holesSolved u1 || holesSolved u2)
   94 |                             (namesSolved u1 ++ namesSolved u2)
   95 |                             NoLazy -- only top level, so assume no annotation
   96 | 
   97 | unionAll : List UnifyResult -> UnifyResult
   98 | unionAll [] = MkUnifyResult [] False [] NoLazy
   99 | unionAll [c] = c
  100 | unionAll (c :: cs) = union c (unionAll cs)
  101 | 
  102 | constrain : Int -> UnifyResult
  103 | constrain c = MkUnifyResult [c] False [] NoLazy
  104 | 
  105 | success : UnifyResult
  106 | success = MkUnifyResult [] False [] NoLazy
  107 | 
  108 | solvedHole : Int -> UnifyResult
  109 | solvedHole n = MkUnifyResult [] True [n] NoLazy
  110 | 
  111 | public export
  112 | interface Unify tm where
  113 |   -- Unify returns a list of ids referring to newly added constraints
  114 |   unifyD : {vars : Scope} ->
  115 |            Ref Ctxt Defs ->
  116 |            Ref UST UState ->
  117 |            UnifyInfo ->
  118 |            FC -> Env Term vars ->
  119 |            tm vars -> tm vars ->
  120 |            Core UnifyResult
  121 |   -- As unify but at the top level can allow lazy/non-lazy to be mixed in
  122 |   -- order to infer annotations
  123 |   unifyWithLazyD : {vars : _} ->
  124 |                    Ref Ctxt Defs ->
  125 |                    Ref UST UState ->
  126 |                    UnifyInfo ->
  127 |                    FC -> Env Term vars ->
  128 |                    tm vars -> tm vars ->
  129 |                    Core UnifyResult
  130 |   unifyWithLazyD = unifyD
  131 | 
  132 | -- Workaround for auto implicits not working in interfaces
  133 | -- In calls to unification, the first argument is the given type, and the second
  134 | -- argument is the expected type.
  135 | export
  136 | unify : Unify tm =>
  137 |         {vars : _} ->
  138 |         {auto c : Ref Ctxt Defs} ->
  139 |         {auto u : Ref UST UState} ->
  140 |         UnifyInfo ->
  141 |         FC -> Env Term vars ->
  142 |         tm vars -> tm vars ->
  143 |         Core UnifyResult
  144 | unify {c} {u} = unifyD c u
  145 | 
  146 | export
  147 | unifyWithLazy : Unify tm =>
  148 |                 {vars : _} ->
  149 |                 {auto c : Ref Ctxt Defs} ->
  150 |                 {auto u : Ref UST UState} ->
  151 |                 UnifyInfo ->
  152 |                 FC -> Env Term vars ->
  153 |                 tm vars -> tm vars ->
  154 |                 Core UnifyResult
  155 | unifyWithLazy {c} {u} = unifyWithLazyD c u
  156 | 
  157 | -- Defined in Core.AutoSearch
  158 | export
  159 | search : {vars : _} ->
  160 |          {auto c : Ref Ctxt Defs} ->
  161 |          {auto u : Ref UST UState} ->
  162 |          FC -> RigCount ->
  163 |          (defaults : Bool) -> (depth : Nat) ->
  164 |          (defining : Name) -> (topTy : Term vars) -> Env Term vars ->
  165 |          Core (Term vars)
  166 | 
  167 | ufail : FC -> String -> Core a
  168 | ufail loc msg = throw (GenericMsg loc msg)
  169 | 
  170 | convertError : {vars : _} ->
  171 |                {auto c : Ref Ctxt Defs} ->
  172 |                FC -> Env Term vars -> NF vars -> NF vars -> Core a
  173 | convertError loc env x y
  174 |     = do defs <- get Ctxt
  175 |          empty <- clearDefs defs
  176 |          throw (CantConvert loc (gamma defs)
  177 |                                 env !(quote empty env x)
  178 |                                     !(quote empty env y))
  179 | 
  180 | convertErrorS : {vars : _} ->
  181 |                 {auto c : Ref Ctxt Defs} ->
  182 |                 Bool -> FC -> Env Term vars -> NF vars -> NF vars -> Core a
  183 | convertErrorS s loc env x y
  184 |     = if s then convertError loc env y x
  185 |            else convertError loc env x y
  186 | 
  187 | -- Find all the metavariables required by each of the given names.
  188 | -- We'll assume all meta solutions are of the form STerm exp.
  189 | chaseMetas : {auto c : Ref Ctxt Defs} ->
  190 |              List Name -> NameMap () -> Core (List Name)
  191 | chaseMetas [] all = pure (keys all)
  192 | chaseMetas (n :: ns) all
  193 |     = case lookup n all of
  194 |            Just _ => chaseMetas ns all
  195 |            _ => do defs <- get Ctxt
  196 |                    Just (PMDef _ _ (STerm _ soln) _ _) <-
  197 |                                   lookupDefExact n (gamma defs)
  198 |                         | _ => chaseMetas ns (insert n () all)
  199 |                    let sns = keys (getMetas soln)
  200 |                    chaseMetas (sns ++ ns) (insert n () all)
  201 | 
  202 | -- Get all the metavariable names used by the term (recursively, so we
  203 | -- can do the occurs check)
  204 | getMetaNames : {auto c : Ref Ctxt Defs} ->
  205 |                Term vars -> Core (List Name)
  206 | getMetaNames tm
  207 |     = let metas = getMetas tm in
  208 |           chaseMetas (keys metas) empty
  209 | 
  210 | postpone : {vars : _} ->
  211 |            {auto c : Ref Ctxt Defs} ->
  212 |            {auto u : Ref UST UState} ->
  213 |            FC -> UnifyInfo -> String ->
  214 |            Env Term vars -> NF vars -> NF vars -> Core UnifyResult
  215 | postpone loc mode logstr env x y
  216 |     = do defs <- get Ctxt
  217 |          empty <- clearDefs defs
  218 |          logC "unify.postpone" 10 $
  219 |               do xq <- quote defs env x
  220 |                  yq <- quote defs env y
  221 |                  pure (logstr ++ ": " ++ show !(toFullNames xq) ++
  222 |                                     " =?= " ++ show !(toFullNames yq))
  223 | 
  224 |          -- If we're blocked because a name is undefined, give up
  225 |          checkDefined defs x
  226 |          checkDefined defs y
  227 | 
  228 |          c <- addConstraint (MkConstraint loc (atTop mode) env x y)
  229 |          log "unify.postpone" 10 $
  230 |                  show c ++ " NEW CONSTRAINT " ++ show loc
  231 |          logNF "unify.postpone" 10 "X" env x
  232 |          logNF "unify.postpone" 10 "Y" env y
  233 |          pure (constrain c)
  234 |   where
  235 |     checkDefined : Defs -> NF vars -> Core ()
  236 |     checkDefined defs (NApp _ (NRef _ n) _)
  237 |         = do Just _ <- lookupCtxtExact n (gamma defs)
  238 |                   | _ => undefinedName loc n
  239 |              pure ()
  240 |     checkDefined _ _ = pure ()
  241 | 
  242 |     undefinedN : Name -> Core Bool
  243 |     undefinedN n
  244 |         = do defs <- get Ctxt
  245 |              pure $ case !(lookupDefExact n (gamma defs)) of
  246 |                   Just (Hole {}) => True
  247 |                   Just (BySearch {}) => True
  248 |                   Just (Guess {}) => True
  249 |                   _ => False
  250 | 
  251 | postponeS : {vars : _} ->
  252 |             {auto c : Ref Ctxt Defs} ->
  253 |             {auto u : Ref UST UState} ->
  254 |             Bool -> FC -> UnifyInfo -> String -> Env Term vars ->
  255 |             NF vars -> NF vars ->
  256 |             Core UnifyResult
  257 | postponeS s loc mode logstr env x y
  258 |     = if s then postpone loc (lower mode) logstr env y x
  259 |            else postpone loc mode logstr env x y
  260 | 
  261 | unifyArgs : (Unify tm, Quote tm) =>
  262 |             {vars : _} ->
  263 |             {auto c : Ref Ctxt Defs} ->
  264 |             {auto u : Ref UST UState} ->
  265 |             UnifyInfo -> FC -> Env Term vars ->
  266 |             List (tm vars) -> List (tm vars) ->
  267 |             Core UnifyResult
  268 | unifyArgs mode loc env [] [] = pure success
  269 | unifyArgs mode loc env (cx :: cxs) (cy :: cys)
  270 |     = do -- Do later arguments first, since they may depend on earlier
  271 |          -- arguments and use their solutions.
  272 |          cs <- unifyArgs mode loc env cxs cys
  273 |          res <- unify (lower mode) loc env cx cy
  274 |          pure (union res cs)
  275 | unifyArgs mode loc env _ _ = ufail loc ""
  276 | 
  277 | -- Get the variables in an application argument list; fail if any arguments
  278 | -- are not variables, fail if there's any repetition of variables
  279 | -- We use this to check that the pattern unification rule is applicable
  280 | -- when solving a metavariable applied to arguments
  281 | -- We return a list (because the order matters) and a set (for easy
  282 | -- querying)
  283 | getVars : List (NF vars) -> Maybe (List (Var vars), VarSet vars)
  284 | getVars = go [<] VarSet.empty where
  285 | 
  286 |   go : SnocList (Var vars) -> VarSet vars ->
  287 |        List (NF vars) -> Maybe (List (Var vars), VarSet vars)
  288 |   go acc got [] = Just (acc <>> [], got)
  289 |   go acc got (NErased fc (Dotted t) :: xs) = go acc got (t :: xs)
  290 |   go acc got (NApp fc (NLocal r idx p) [] :: xs)
  291 |     = let v := MkVar p in
  292 |       if v `VarSet.elem` got then Nothing
  293 |          else go (acc :< v) (VarSet.insert v got) xs
  294 |   go acc got (NAs _ _ _ p :: xs) = go acc got (p :: xs)
  295 |   go acc _ (_ :: xs) = Nothing
  296 | 
  297 | -- Update the variable list to point into the sub environment
  298 | -- (All of these will succeed because the Thin we have comes from
  299 | -- the list of variable uses! It's not stated in the type, though.)
  300 | updateVars : List (Var {a = Name} vars) -> Thin newvars vars -> List (Var newvars)
  301 | updateVars vs th = mapMaybe (\ v => shrink v th) vs
  302 | 
  303 | {- Applying the pattern unification rule is okay if:
  304 |    * Arguments are all distinct local variables
  305 |    * The metavariable name doesn't appear in the unifying term
  306 |    * The local variables which appear in the term are all arguments to
  307 |      the metavariable application (not checked here, checked with the
  308 |      result of `patternEnv`)
  309 | 
  310 |    Return the subset of the environment used in the arguments
  311 |    to which the metavariable is applied. If this environment is enough
  312 |    to check the term we're unifying with, and that term doesn't use the
  313 |    metavariable name, we can safely apply the rule.
  314 | 
  315 |    Also, return the list of arguments the metavariable was applied to, to
  316 |    make sure we use them in the right order when we build the solution.
  317 | -}
  318 | patternEnv : {auto c : Ref Ctxt Defs} ->
  319 |              {auto u : Ref UST UState} ->
  320 |              {vars : _} ->
  321 |              Env Term vars -> List (Closure vars) ->
  322 |              Core (Maybe (newvars ** (List (Var newvars),
  323 |                                      Thin newvars vars)))
  324 | patternEnv {vars} env args
  325 |     = do defs <- get Ctxt
  326 |          empty <- clearDefs defs
  327 |          args' <- traverse (evalArg empty) args
  328 |          pure $
  329 |            case getVars args' of
  330 |              Nothing => Nothing
  331 |              Just (vslist, vsset) =>
  332 |                let (newvars ** svs) = fromVarSet _ vsset in
  333 |                  Just (newvars ** (updateVars vslist svs, svs))
  334 | 
  335 | getVarsTm : List (Term vars) -> Maybe (List (Var vars), VarSet vars)
  336 | getVarsTm = go [<] VarSet.empty where
  337 | 
  338 |   go : SnocList (Var vars) -> VarSet vars ->
  339 |        List (Term vars) -> Maybe (List (Var vars), VarSet vars)
  340 |   go acc got [] = Just (acc <>> [], got)
  341 |   go acc got (Local fc r idx p :: xs)
  342 |     = let v := MkVar p in
  343 |       if v `VarSet.elem` got then Nothing
  344 |          else go (acc :< v) (VarSet.insert v got) xs
  345 |   go acc _ (_ :: xs) = Nothing
  346 | 
  347 | export
  348 | patternEnvTm : {auto c : Ref Ctxt Defs} ->
  349 |                {auto u : Ref UST UState} ->
  350 |                {vars : _} ->
  351 |                Env Term vars -> List (Term vars) ->
  352 |                Core (Maybe (newvars ** (List (Var newvars),
  353 |                                        Thin newvars vars)))
  354 | patternEnvTm {vars} env args
  355 |     = do defs <- get Ctxt
  356 |          empty <- clearDefs defs
  357 |          pure $ case getVarsTm args of
  358 |            Nothing => Nothing
  359 |            Just (vslist, vsset) =>
  360 |              let (newvars ** svs) = fromVarSet _ vsset in
  361 |                  Just (newvars ** (updateVars vslist svs, svs))
  362 | 
  363 | -- Check that the metavariable name doesn't occur in the solution.
  364 | -- If it does, normalising might help. If it still does, that's an error.
  365 | occursCheck : {vars : _} ->
  366 |               {auto c : Ref Ctxt Defs} ->
  367 |               FC -> Env Term vars -> UnifyInfo ->
  368 |               Name -> Term vars -> Core (Maybe (Term vars))
  369 | occursCheck fc env mode mname tm
  370 |     = do solmetas <- getMetaNames tm
  371 |          let False = mname `elem` solmetas
  372 |              | _ => do defs <- get Ctxt
  373 |                        tmnf <- normalise defs env tm
  374 |                        solmetas <- getMetaNames tmnf
  375 |                        if mname `elem` solmetas
  376 |                           then do failOnStrongRigid False
  377 |                                      (throw (CyclicMeta fc env mname tmnf))
  378 |                                      tmnf
  379 |                                   pure Nothing
  380 |                           else pure $ Just tmnf
  381 |          pure $ Just tm
  382 |   where
  383 |     -- Throw an occurs check failure if the name appears 'strong rigid',
  384 |     -- that is, under a constructor form rather than a function, in the
  385 |     -- term
  386 |     failOnStrongRigid : Bool -> Core () -> Term vars -> Core ()
  387 |     failOnStrongRigid bad err (Meta _ n _ _)
  388 |         = if bad && n == mname
  389 |              then err
  390 |              else pure ()
  391 |     failOnStrongRigid bad err tm
  392 |         = case getFnArgs tm of
  393 |                (f, []) => pure ()
  394 |                (Ref _ Func _, _) => pure () -- might reduce away, just block
  395 |                (Ref _ _ _, args) => traverse_ (failOnStrongRigid True err) args
  396 |                (f, args) => traverse_ (failOnStrongRigid bad err) args
  397 | 
  398 | -- How the variables in a metavariable definition map to the variables in
  399 | -- the solution term (the Var newvars)
  400 | --
  401 | -- TODO factor out as a renaming
  402 | -- TODO use `All` "quantifier"
  403 | data IVars : Scope -> Scoped where
  404 |      INil : IVars Scope.empty newvars
  405 |      ICons : Maybe (Var newvars) -> IVars vs newvars ->
  406 |              IVars (v :: vs) newvars
  407 | 
  408 | Weaken (IVars vs) where
  409 |   weakenNs s INil = INil
  410 |   weakenNs s (ICons t ts) = ICons (weakenNs @{MaybeWeaken} s t) (weakenNs s ts)
  411 | 
  412 | getIVars : IVars vs ns -> List (Maybe (Var ns))
  413 | getIVars INil = []
  414 | getIVars (ICons v vs) = v :: getIVars vs
  415 | 
  416 | -- Instantiate a metavariable by binding the variables in 'newvars'
  417 | -- and returning the term
  418 | -- If the type of the metavariable doesn't have enough arguments, fail, because
  419 | -- this wasn't valid for pattern unification
  420 | tryInstantiate : {auto c : Ref Ctxt Defs} ->
  421 |               {auto u : Ref UST UState} ->
  422 |               {vars, newvars : _} ->
  423 |               FC -> UnifyInfo -> Env Term vars ->
  424 |               (metavar : Name) -> (mref : Int) -> (numargs : Nat) ->
  425 |               (mdef : GlobalDef) ->
  426 |               List (Var newvars) -> -- Variable each argument maps to
  427 |               Term vars -> -- original, just for error message
  428 |               Term newvars -> -- shrunk environment
  429 |               Core Bool -- postpone if the type is yet unknown
  430 | tryInstantiate {newvars} loc mode env mname mref num mdef locs otm tm
  431 |     = do logTerm "unify.instantiate" 5 ("Instantiating in " ++ show newvars) tm
  432 | --          let Hole _ _ = definition mdef
  433 | --              | def => ufail {a=()} loc (show mname ++ " already resolved as " ++ show def)
  434 |          case fullname mdef of
  435 |               PV pv pi => throw (PatternVariableUnifies loc (getLoc otm) env (PV pv pi) otm)
  436 |               _ => pure ()
  437 |          defs <- get Ctxt
  438 |          ty <- normalisePis defs Env.empty $ type mdef
  439 |                      -- make sure we have all the pi binders we need in the
  440 |                      -- type to make the metavariable definition
  441 |          logTerm "unify.instantiate" 5 ("Type: " ++ show mname) (type mdef)
  442 |          logTerm "unify.instantiate" 5 ("Type: " ++ show mname) ty
  443 |          log "unify.instantiate" 5 ("With locs: " ++ show locs)
  444 |          log "unify.instantiate" 5 ("From vars: " ++ show newvars)
  445 | 
  446 |          defs <- get Ctxt
  447 |          -- Try to instantiate the hole
  448 |          Just rhs <- mkDef locs INil tm ty
  449 |            | _ => do
  450 |                log "unify.instantiate" 5 "Postponed"
  451 |                pure False
  452 | 
  453 |          logTerm "unify.instantiate" 5 "Definition" rhs
  454 |          let simpleDef = MkPMDefInfo (SolvedHole num)
  455 |                                      (not (isUserName mname) && isSimple rhs)
  456 |                                      False
  457 |          let newdef = { definition :=
  458 |                           PMDef simpleDef Scope.empty (STerm 0 rhs) (STerm 0 rhs) []
  459 |                       } mdef
  460 |          ignore $ addDef (Resolved mref) newdef
  461 |          removeHole mref
  462 |          pure True
  463 |   where
  464 |     precise : Bool
  465 |     precise
  466 |         = case definition mdef of
  467 |                Hole _ p => precisetype p
  468 |                _ => False
  469 | 
  470 |     -- A solution is deemed simple enough to inline if either:
  471 |     --   * It is smaller than some threshold and has no metavariables in it
  472 |     --   * It's just a metavariable itself
  473 |     noMeta : Term vs -> Nat -> Bool
  474 |     noMeta (App _ f a) (S k) = noMeta f k && noMeta a k
  475 |     noMeta (Bind _ _ b sc) (S k) = noMeta (binderType b) k && noMeta sc k
  476 |     noMeta (Meta {}) d = False
  477 |     noMeta (TDelayed _ _ t) d = noMeta t d
  478 |     noMeta (TDelay _ _ t a) d = noMeta t d && noMeta a d
  479 |     noMeta (TForce _ _ t) d = noMeta t d
  480 |     noMeta (As _ _ a p) d = noMeta a d && noMeta p d
  481 |     noMeta (Local {}) _ = True
  482 |     noMeta (Ref {}) _ = True
  483 |     noMeta (PrimVal {}) _ = True
  484 |     noMeta (TType {}) _ = True
  485 |     noMeta _ _ = False
  486 | 
  487 |     isSimple : Term vs -> Bool
  488 |     isSimple (Meta {}) = True
  489 |     isSimple (Bind _ _ (Lam {}) sc) = isSimple sc
  490 |     isSimple (App _ f a) = noMeta f 6 && noMeta a 3
  491 |     isSimple tm = noMeta tm 0
  492 | 
  493 |     updateIVar : forall vs, newvars . IVars vs newvars -> Var newvars ->
  494 |                  Maybe (Var vs)
  495 |     updateIVar (ICons Nothing rest) new
  496 |         = later <$> updateIVar rest new
  497 |     updateIVar (ICons (Just old) rest) new
  498 |         = if new == old
  499 |              then Just first
  500 |              else later <$> updateIVar rest new
  501 |     updateIVar _ _ = Nothing
  502 | 
  503 |     updateIVars : {vs, newvars : _} ->
  504 |                   IVars vs newvars -> Term newvars -> Maybe (Term vs)
  505 |     updateIVars ivs (Local fc r idx p)
  506 |         = do MkVar p' <- updateIVar ivs (MkVar p)
  507 |              Just (Local fc r _ p')
  508 |     updateIVars ivs (Ref fc nt n) = pure $ Ref fc nt n
  509 |     updateIVars ivs (Meta fc n i args)
  510 |         = pure $ Meta fc n i !(traverse (updateIVars ivs) args)
  511 |     updateIVars {vs} ivs (Bind fc x b sc)
  512 |         = do b' <- updateIVarsB ivs b
  513 |              sc' <- updateIVars (ICons (Just first) (weaken ivs)) sc
  514 |              Just (Bind fc x b' sc')
  515 |       where
  516 |         updateIVarsPi : {vs, newvars : _} ->
  517 |                         IVars vs newvars -> PiInfo (Term newvars) -> Maybe (PiInfo (Term vs))
  518 |         updateIVarsPi ivs Explicit = Just Explicit
  519 |         updateIVarsPi ivs Implicit = Just Implicit
  520 |         updateIVarsPi ivs AutoImplicit = Just AutoImplicit
  521 |         updateIVarsPi ivs (DefImplicit t)
  522 |             = do t' <- updateIVars ivs t
  523 |                  Just (DefImplicit t')
  524 | 
  525 |         updateIVarsB : {vs, newvars : _} ->
  526 |                        IVars vs newvars -> Binder (Term newvars) -> Maybe (Binder (Term vs))
  527 |         updateIVarsB ivs (Lam fc c p t)
  528 |             = do p' <- updateIVarsPi ivs p
  529 |                  Just (Lam fc c p' !(updateIVars ivs t))
  530 |         updateIVarsB ivs (Let fc c v t) = Just (Let fc c !(updateIVars ivs v) !(updateIVars ivs t))
  531 |         -- Make 'pi' binders have multiplicity W when we infer a Rig1 metavariable,
  532 |         -- since this is the most general thing to do if it's unknown.
  533 |         updateIVarsB ivs (Pi fc rig p t)
  534 |             = do p' <- updateIVarsPi ivs p
  535 |                  Just (Pi fc rig p' !(updateIVars ivs t))
  536 |         updateIVarsB ivs (PVar fc c p t)
  537 |             = do p' <- updateIVarsPi ivs p
  538 |                  Just (PVar fc c p' !(updateIVars ivs t))
  539 |         updateIVarsB ivs (PLet fc c v t) = Just (PLet fc c !(updateIVars ivs v) !(updateIVars ivs t))
  540 |         updateIVarsB ivs (PVTy fc c t) = Just (PVTy fc c !(updateIVars ivs t))
  541 |     updateIVars ivs (App fc f a)
  542 |         = Just (App fc !(updateIVars ivs f) !(updateIVars ivs a))
  543 |     updateIVars ivs (As fc u a p)
  544 |         = Just (As fc u !(updateIVars ivs a) !(updateIVars ivs p))
  545 |     updateIVars ivs (TDelayed fc r arg)
  546 |         = Just (TDelayed fc r !(updateIVars ivs arg))
  547 |     updateIVars ivs (TDelay fc r ty arg)
  548 |         = Just (TDelay fc r !(updateIVars ivs ty) !(updateIVars ivs arg))
  549 |     updateIVars ivs (TForce fc r arg)
  550 |         = Just (TForce fc r !(updateIVars ivs arg))
  551 |     updateIVars ivs (PrimVal fc c) = Just (PrimVal fc c)
  552 |     updateIVars ivs (Erased fc Impossible) = Just (Erased fc Impossible)
  553 |     updateIVars ivs (Erased fc Placeholder) = Just (Erased fc Placeholder)
  554 |     updateIVars ivs (Erased fc (Dotted t)) = Erased fc . Dotted <$> updateIVars ivs t
  555 |     updateIVars ivs (TType fc u) = Just (TType fc u)
  556 | 
  557 |     mkDef : {vs, newvars : _} ->
  558 |             List (Var newvars) ->
  559 |             IVars vs newvars -> Term newvars -> Term vs ->
  560 |             Core (Maybe (Term vs))
  561 |     mkDef (v :: vs) vars soln (Bind bfc x (Pi fc c info ty) sc)
  562 |        = do sc' <- mkDef vs (ICons (Just v) vars) soln sc
  563 |             pure $ (Bind bfc x (Lam fc c info (Erased bfc Placeholder)) <$> sc')
  564 |     mkDef vs vars soln (Bind bfc x b@(Let _ c val ty) sc)
  565 |        = do mbsc' <- mkDef vs (ICons Nothing vars) soln sc
  566 |             flip traverseOpt mbsc' $ \sc' =>
  567 |               case shrink sc' (Drop Refl) of
  568 |                 Just scs => pure scs
  569 |                 Nothing => pure $ Bind bfc x b sc'
  570 |     mkDef [] vars soln _
  571 |        = do let Just soln' = updateIVars vars soln
  572 |                 | Nothing => ufail loc ("Can't make solution for " ++ show mname
  573 |                                            ++ " " ++ show (getIVars vars, soln))
  574 |             pure (Just soln')
  575 |     mkDef _ _ _ _ = pure Nothing
  576 | 
  577 | -- update a solution that the machine found with the thing the programmer
  578 | -- actually wrote! We assume that we've already checked that they unify.
  579 | export
  580 | updateSolution : {vars : _} ->
  581 |                  {auto c : Ref Ctxt Defs} ->
  582 |                  {auto u : Ref UST UState} ->
  583 |                  Env Term vars -> Term vars -> Term vars -> Core Bool
  584 | updateSolution env (Meta fc mname idx args) soln
  585 |     = do defs <- get Ctxt
  586 |          case !(patternEnvTm env args) of
  587 |               Nothing => pure False
  588 |               Just (newvars ** (locs, submv)) =>
  589 |                   case shrink soln submv of
  590 |                        Nothing => pure False
  591 |                        Just stm =>
  592 |                           do Just hdef <- lookupCtxtExact (Resolved idx) (gamma defs)
  593 |                                   | Nothing => throw (InternalError "Can't happen: no definition")
  594 |                              tryInstantiate fc inTerm env mname idx (length args) hdef (toList locs) soln stm
  595 | updateSolution env metavar soln
  596 |     = pure False
  597 | 
  598 | export
  599 | solveIfUndefined : {vars : _} ->
  600 |                    {auto c : Ref Ctxt Defs} ->
  601 |                    {auto u : Ref UST UState} ->
  602 |                    Env Term vars -> Term vars -> Term vars -> Core Bool
  603 | solveIfUndefined env metavar@(Meta fc mname idx args) soln
  604 |     = do defs <- get Ctxt
  605 |          Just (Hole {}) <- lookupDefExact (Resolved idx) (gamma defs)
  606 |               | _ => pure False
  607 |          updateSolution env metavar soln
  608 | solveIfUndefined env (Erased _ (Dotted metavar)) soln
  609 |   = solveIfUndefined env metavar soln
  610 | solveIfUndefined env metavar soln
  611 |     = pure False
  612 | 
  613 | isDefInvertible : {auto c : Ref Ctxt Defs} ->
  614 |                   FC -> Int -> Core Bool
  615 | isDefInvertible fc i
  616 |     = do defs <- get Ctxt
  617 |          Just gdef <- lookupCtxtExact (Resolved i) (gamma defs)
  618 |               | Nothing => throw (UndefinedName fc (Resolved i))
  619 |          pure (invertible gdef)
  620 | 
  621 | mutual
  622 |   unifyIfEq : {auto c : Ref Ctxt Defs} ->
  623 |               {auto u : Ref UST UState} ->
  624 |               {vars : _} ->
  625 |               (postpone : Bool) ->
  626 |               FC -> UnifyInfo -> Env Term vars -> NF vars -> NF vars ->
  627 |               Core UnifyResult
  628 |   unifyIfEq post loc mode env x y
  629 |         = do defs <- get Ctxt
  630 |              if !(convertInf defs env x y)
  631 |                 then pure success
  632 |                 else if post
  633 |                         then postpone loc mode ("Postponing unifyIfEq " ++
  634 |                                                  show (atTop mode)) env x y
  635 |                         else convertError loc env x y
  636 | 
  637 |   getArgTypes : {vars : _} ->
  638 |                 {auto c : Ref Ctxt Defs} ->
  639 |                 Defs -> (fnType : NF vars) -> List (Closure vars) ->
  640 |                 Core (Maybe (List (NF vars)))
  641 |   getArgTypes defs (NBind _ n (Pi _ _ _ ty) sc) (a :: as)
  642 |      = do Just scTys <- getArgTypes defs !(sc defs a) as
  643 |                | Nothing => pure Nothing
  644 |           pure (Just (!(evalClosure defs ty) :: scTys))
  645 |   getArgTypes _ _ [] = pure (Just [])
  646 |   getArgTypes _ _ _ = pure Nothing
  647 | 
  648 |   headsConvert : {vars : _} ->
  649 |                  {auto c : Ref Ctxt Defs} ->
  650 |                  {auto u : Ref UST UState} ->
  651 |                  UnifyInfo ->
  652 |                  FC -> Env Term vars ->
  653 |                  Maybe (List (NF vars)) -> Maybe (List (NF vars)) ->
  654 |                  Core Bool
  655 |   headsConvert mode fc env (Just vs) (Just ns)
  656 |       = case (reverse vs, reverse ns) of
  657 |              (v :: _, n :: _) =>
  658 |                 do logNF "unify.head" 10 "Unifying head" env v
  659 |                    logNF "unify.head" 10 ".........with" env n
  660 |                    res <- unify mode fc env v n
  661 |                    -- If there's constraints, we postpone the whole equation
  662 |                    -- so no need to record them
  663 |                    pure (isNil (constraints res ))
  664 |              _ => pure False
  665 |   headsConvert mode fc env _ _
  666 |       = do log "unify.head" 10 "Nothing to convert"
  667 |            pure True
  668 | 
  669 |   unifyInvertible : {auto c : Ref Ctxt Defs} ->
  670 |                     {auto u : Ref UST UState} ->
  671 |                     {vars : _} ->
  672 |                     (swaporder : Bool) ->
  673 |                     UnifyInfo -> FC -> Env Term vars ->
  674 |                     (metaname : Name) -> (metaref : Int) ->
  675 |                     (margs : List (Closure vars)) ->
  676 |                     (margs' : List (Closure vars)) ->
  677 |                     Maybe ClosedTerm ->
  678 |                     (List (FC, Closure vars) -> NF vars) ->
  679 |                     List (FC, Closure vars) ->
  680 |                     Core UnifyResult
  681 |   unifyInvertible swap mode fc env mname mref margs margs' nty con args'
  682 |       = do defs <- get Ctxt
  683 |            -- Get the types of the arguments to ensure that the rightmost
  684 |            -- argument types match up
  685 |            Just vty <- lookupTyExact (Resolved mref) (gamma defs)
  686 |                 | Nothing => ufail fc ("No such metavariable " ++ show mname)
  687 |            vargTys <- getArgTypes defs !(nf defs env (embed vty)) (margs ++ margs')
  688 |            nargTys <- maybe (pure Nothing)
  689 |                             (\ty => getArgTypes defs !(nf defs env (embed ty)) $ map snd args')
  690 |                             nty
  691 |            -- If the rightmost arguments have the same type, or we don't
  692 |            -- know the types of the arguments, we'll get on with it.
  693 |            if !(headsConvert mode fc env vargTys nargTys)
  694 |               then
  695 |                 -- Unify the rightmost arguments, with the goal of turning the
  696 |                 -- hole application into a pattern form
  697 |                 case (reverse margs', reverse args') of
  698 |                      (h :: hargs, f :: fargs) =>
  699 |                         tryUnify
  700 |                           (if not swap then
  701 |                               do log "unify.invertible" 10 "Unifying invertible"
  702 |                                  ures <- unify mode fc env h (snd f)
  703 |                                  log "unify.invertible" 10 $ "Constraints " ++ show (constraints ures)
  704 |                                  uargs <- unify mode fc env
  705 |                                        (NApp fc (NMeta mname mref margs) (reverse $ map (EmptyFC,) hargs))
  706 |                                        (con (reverse fargs))
  707 |                                  pure (union ures uargs)
  708 |                              else
  709 |                               do log "unify.invertible" 10 "Unifying invertible"
  710 |                                  ures <- unify mode fc env (snd f) h
  711 |                                  log "unify.invertible" 10 $ "Constraints " ++ show (constraints ures)
  712 |                                  uargs <- unify mode fc env
  713 |                                        (con (reverse fargs))
  714 |                                        (NApp fc (NMeta mname mref margs) (reverse $ map (EmptyFC,) hargs))
  715 |                                  pure (union ures uargs))
  716 |                           (postponeS swap fc mode "Postponing hole application [1]" env
  717 |                                 (NApp fc (NMeta mname mref margs) $ map (EmptyFC,) margs')
  718 |                                 (con args'))
  719 |                      _ => postponeS swap fc mode "Postponing hole application [2]" env
  720 |                                 (NApp fc (NMeta mname mref margs) (map (EmptyFC,) margs'))
  721 |                                 (con args')
  722 |               else -- TODO: Cancellable function applications
  723 |                    postpone fc mode "Postponing hole application [3]" env
  724 |                             (NApp fc (NMeta mname mref margs) (map (EmptyFC,) margs')) (con args')
  725 | 
  726 |   -- Unify a hole application - we have already checked that the hole is
  727 |   -- invertible (i.e. it's a determining argument to a proof search where
  728 |   -- it is a constructor or something else invertible in each case)
  729 |   unifyHoleApp : {auto c : Ref Ctxt Defs} ->
  730 |                  {auto u : Ref UST UState} ->
  731 |                  {vars : _} ->
  732 |                  (swaporder : Bool) ->
  733 |                  UnifyInfo -> FC -> Env Term vars ->
  734 |                  (metaname : Name) -> (metaref : Int) ->
  735 |                  (margs : List (Closure vars)) ->
  736 |                  (margs' : List (Closure vars)) ->
  737 |                  NF vars ->
  738 |                  Core UnifyResult
  739 |   unifyHoleApp swap mode loc env mname mref margs margs' (NTCon nfc n a args')
  740 |       = do defs <- get Ctxt
  741 |            mty <- lookupTyExact n (gamma defs)
  742 |            unifyInvertible swap (lower mode) loc env mname mref margs margs' mty (NTCon nfc n a) args'
  743 |   unifyHoleApp swap mode loc env mname mref margs margs' (NDCon nfc n t a args')
  744 |       = do defs <- get Ctxt
  745 |            mty <- lookupTyExact n (gamma defs)
  746 |            unifyInvertible swap (lower mode) loc env mname mref margs margs' mty (NDCon nfc n t a) args'
  747 |   unifyHoleApp swap mode loc env mname mref margs margs' (NApp nfc (NLocal r idx p) args')
  748 |       = unifyInvertible swap (lower mode) loc env mname mref margs margs' Nothing
  749 |                         (NApp nfc (NLocal r idx p)) args'
  750 |   unifyHoleApp swap mode loc env mname mref margs margs' tm@(NApp nfc (NMeta n i margs2) args2')
  751 |       = do defs <- get Ctxt
  752 |            Just mdef <- lookupCtxtExact (Resolved i) (gamma defs)
  753 |                 | Nothing => undefinedName nfc mname
  754 |            let inv = isPatName n || invertible mdef
  755 |            if inv
  756 |               then unifyInvertible swap (lower mode) loc env mname mref margs margs' Nothing
  757 |                                    (NApp nfc (NMeta n i margs2)) args2'
  758 |               else postponeS swap loc mode "Postponing hole application" env
  759 |                              (NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs') tm
  760 |     where
  761 |       isPatName : Name -> Bool
  762 |       isPatName (PV {}) = True
  763 |       isPatName _ = False
  764 | 
  765 |   unifyHoleApp swap mode loc env mname mref margs margs' tm
  766 |       = postponeS swap loc mode "Postponing hole application" env
  767 |                  (NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs') tm
  768 | 
  769 |   postponePatVar : {auto c : Ref Ctxt Defs} ->
  770 |                    {auto u : Ref UST UState} ->
  771 |                    {vars : _} ->
  772 |                    (swaporder : Bool) ->
  773 |                    UnifyInfo -> FC -> Env Term vars ->
  774 |                    (metaname : Name) -> (metaref : Int) ->
  775 |                    (margs : List (Closure vars)) ->
  776 |                    (margs' : List (Closure vars)) ->
  777 |                    (soln : NF vars) ->
  778 |                    Core UnifyResult
  779 |   postponePatVar swap mode loc env mname mref margs margs' tm
  780 |       = do let x = NApp loc (NMeta mname mref margs) (map (EmptyFC,) margs')
  781 |            defs <- get Ctxt
  782 |            if !(convert defs env x tm)
  783 |               then pure success
  784 |               else postponeS swap loc mode "Not in pattern fragment" env
  785 |                              x tm
  786 | 
  787 |   solveHole : {auto c : Ref Ctxt Defs} ->
  788 |               {auto u : Ref UST UState} ->
  789 |               {newvars, vars : _} ->
  790 |               FC -> UnifyInfo -> Env Term vars ->
  791 |               (metaname : Name) -> (metaref : Int) ->
  792 |               (margs : List (Closure vars)) ->
  793 |               (margs' : List (Closure vars)) ->
  794 |               List (Var newvars) ->
  795 |               Thin newvars vars ->
  796 |               (solfull : Term vars) -> -- Original solution
  797 |               (soln : Term newvars) -> -- Solution with shrunk environment
  798 |               (solnf : NF vars) ->
  799 |               Core (Maybe UnifyResult)
  800 |   solveHole loc mode env mname mref margs margs' locs submv solfull stm solnf
  801 |       = do defs <- get Ctxt
  802 |            ust <- get UST
  803 |            empty <- clearDefs defs
  804 |            -- if the terms are the same, this isn't a solution
  805 |            -- but they are already unifying, so just return
  806 |            if solutionHeadSame solnf || inNoSolve mref (noSolve ust)
  807 |               then pure $ Just success
  808 |               else -- Rather than doing the occurs check here immediately,
  809 |                    -- we'll wait until all metavariables are resolved, and in
  810 |                    -- the meantime look out for cycles when normalising (which
  811 |                    -- is cheap enough because we only need to look out for
  812 |                    -- metavariables)
  813 |                    do Just hdef <- lookupCtxtExact (Resolved mref) (gamma defs)
  814 |                            | Nothing => throw (InternalError ("Can't happen: Lost hole " ++ show mname))
  815 |                       progress <- tryInstantiate loc mode env mname mref (length margs) hdef (toList locs) solfull stm
  816 |                       pure $ toMaybe progress (solvedHole mref)
  817 |     where
  818 |       inNoSolve : Int -> IntMap () -> Bool
  819 |       inNoSolve i ns
  820 |           = case lookup i ns of
  821 |                  Nothing => False
  822 |                  Just _ => True
  823 | 
  824 |       -- Only need to check the head metavar is the same, we've already
  825 |       -- checked the rest if they are the same (and we couldn't instantiate it
  826 |       -- anyway...)
  827 |       solutionHeadSame : NF vars -> Bool
  828 |       solutionHeadSame (NApp _ (NMeta _ shead _) _) = shead == mref
  829 |       solutionHeadSame _ = False
  830 | 
  831 |   unifyHole : {auto c : Ref Ctxt Defs} ->
  832 |               {auto u : Ref UST UState} ->
  833 |               {vars : _} ->
  834 |               (swaporder : Bool) ->
  835 |               UnifyInfo -> FC -> Env Term vars ->
  836 |               FC -> (metaname : Name) -> (metaref : Int) ->
  837 |               (args : List (Closure vars)) ->
  838 |               (args' : List (Closure vars)) ->
  839 |               (soln : NF vars) ->
  840 |               Core UnifyResult
  841 |   unifyHole swap mode loc env fc mname mref margs margs' tmnf
  842 |       = do defs <- get Ctxt
  843 |            empty <- clearDefs defs
  844 |            let args = if isNil margs' then margs else margs ++ margs'
  845 |            logC "unify.hole" 10
  846 |                    (do args' <- traverse (evalArg empty) args
  847 |                        qargs <- traverse (quote empty env) args'
  848 |                        qtm <- quote empty env tmnf
  849 |                        pure $ "Unifying: " ++ show mname ++ " " ++ show qargs ++
  850 |                               " with " ++ show qtm) -- first attempt, try 'empty', only try 'defs' when on 'retry'?
  851 |            case !(patternEnv env args) of
  852 |                 Nothing =>
  853 |                   do Just hdef <- lookupCtxtExact (Resolved mref) (gamma defs)
  854 |                         | _ => postponePatVar swap mode loc env mname mref margs margs' tmnf
  855 |                      let Hole _ _ = definition hdef
  856 |                         | _ => postponePatVar swap mode loc env mname mref margs margs' tmnf
  857 |                      if invertible hdef
  858 |                         then unifyHoleApp swap mode loc env mname mref margs margs' tmnf
  859 |                         else postponePatVar swap mode loc env mname mref margs margs' tmnf
  860 |                 Just (newvars ** (locs, submv)) =>
  861 |                   do Just hdef <- lookupCtxtExact (Resolved mref) (gamma defs)
  862 |                          | _ => postponePatVar swap mode loc env mname mref margs margs' tmnf
  863 |                      let Hole _ _ = definition hdef
  864 |                          | _ => postponeS swap loc mode "Delayed hole" env
  865 |                                           (NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs')
  866 |                                           tmnf
  867 |                      let qopts = MkQuoteOpts False False
  868 |                                              (Just defs.options.elabDirectives.nfThreshold)
  869 |                      tm <- catch (quoteOpts qopts empty env tmnf)
  870 |                                  (\err => quote defs env tmnf)
  871 |                      Just tm <- occursCheck loc env mode mname tm
  872 |                          | _ => postponeS swap loc mode "Occurs check failed" env
  873 |                                           (NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs')
  874 |                                           tmnf
  875 | 
  876 |                      let solveOrElsePostpone : Term newvars -> Core UnifyResult
  877 |                          solveOrElsePostpone stm = do
  878 |                            mbResult <- solveHole fc mode env mname mref
  879 |                                                  margs margs' locs submv
  880 |                                                  tm stm tmnf
  881 |                            flip fromMaybe (pure <$> mbResult) $
  882 |                              postponeS swap loc mode "Can't instantiate" env
  883 |                                        (NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs') tmnf
  884 | 
  885 |                      case shrink tm submv of
  886 |                           Just stm => solveOrElsePostpone stm
  887 |                           Nothing =>
  888 |                             do tm' <- quote defs env tmnf
  889 |                                case shrink tm' submv of
  890 |                                     Nothing => postponeS swap loc mode "Can't shrink" env
  891 |                                                          (NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs')
  892 |                                                          tmnf
  893 |                                     Just stm => solveOrElsePostpone stm
  894 | 
  895 |   -- Unify an application with something else
  896 |   unifyApp : {auto c : Ref Ctxt Defs} ->
  897 |              {auto u : Ref UST UState} ->
  898 |              {vars : _} ->
  899 |              (swaporder : Bool) -> -- swap the order when postponing
  900 |                                    -- (this is to preserve second arg being expected type)
  901 |              UnifyInfo -> FC -> Env Term vars -> FC ->
  902 |              NHead vars -> List (FC, Closure vars) -> NF vars ->
  903 |              Core UnifyResult
  904 |   unifyApp swap mode loc env fc (NMeta n i margs) args tm
  905 |       = unifyHole swap mode loc env fc n i margs (map snd args) tm
  906 |   unifyApp swap mode loc env fc hd args (NApp mfc (NMeta n i margs) margs')
  907 |       = unifyHole swap mode loc env mfc n i margs (map snd margs') (NApp fc hd args)
  908 |   unifyApp swap mode loc env fc hd args (NErased _ (Dotted t))
  909 |       = unifyApp swap mode loc env fc hd args t
  910 |   -- Postpone if a name application against an application, unless they are
  911 |   -- convertible
  912 |   unifyApp swap mode loc env fc (NRef nt n) args tm
  913 |       = do log "unify.application" 10 $ "Name against app, unifyIfEq"
  914 |            if not swap
  915 |               then unifyIfEq True loc mode env (NApp fc (NRef nt n) args) tm
  916 |               else unifyIfEq True loc mode env tm (NApp fc (NRef nt n) args)
  917 |   unifyApp swap mode loc env xfc (NLocal rx x xp) [] (NApp yfc (NLocal ry y yp) [])
  918 |       = do gam <- get Ctxt
  919 |            if x == y then pure success
  920 |              else postponeS swap loc mode "Postponing var"
  921 |                             env (NApp xfc (NLocal rx x xp) [])
  922 |                                 (NApp yfc (NLocal ry y yp) [])
  923 |   -- A local against something canonical (binder or constructor) is bad
  924 |   unifyApp swap mode loc env xfc (NLocal rx x xp) args y@(NBind {})
  925 |       = convertErrorS swap loc env (NApp xfc (NLocal rx x xp) args) y
  926 |   unifyApp swap mode loc env xfc (NLocal rx x xp) args y@(NDCon {})
  927 |       = convertErrorS swap loc env (NApp xfc (NLocal rx x xp) args) y
  928 |   unifyApp swap mode loc env xfc (NLocal rx x xp) args y@(NTCon {})
  929 |       = convertErrorS swap loc env (NApp xfc (NLocal rx x xp) args) y
  930 |   unifyApp swap mode loc env xfc (NLocal rx x xp) args y@(NPrimVal {})
  931 |       = convertErrorS swap loc env (NApp xfc (NLocal rx x xp) args) y
  932 |   unifyApp swap mode loc env xfc (NLocal rx x xp) args y@(NType {})
  933 |       = convertErrorS swap loc env (NApp xfc (NLocal rx x xp) args) y
  934 |   -- If they're already convertible without metavariables, we're done,
  935 |   -- otherwise postpone
  936 |   unifyApp False mode loc env fc hd args tm
  937 |       = do gam <- get Ctxt
  938 |            if !(convert gam env (NApp fc hd args) tm)
  939 |               then pure success
  940 |               else postponeS False loc mode "Postponing constraint"
  941 |                              env (NApp fc hd args) tm
  942 |   unifyApp True mode loc env fc hd args tm
  943 |       = do gam <- get Ctxt
  944 |            if !(convert gam env tm (NApp fc hd args))
  945 |               then pure success
  946 |               else postponeS True loc mode "Postponing constraint"
  947 |                              env (NApp fc hd args) tm
  948 | 
  949 |   unifyBothApps : {auto c : Ref Ctxt Defs} ->
  950 |                   {auto u : Ref UST UState} ->
  951 |                   {vars : _} ->
  952 |                   UnifyInfo -> FC -> Env Term vars ->
  953 |                   FC -> NHead vars -> List (FC, Closure vars) ->
  954 |                   FC -> NHead vars -> List (FC, Closure vars) ->
  955 |                   Core UnifyResult
  956 |   unifyBothApps mode loc env xfc (NLocal xr x xp) [] yfc (NLocal yr y yp) []
  957 |       = if x == y
  958 |            then pure success
  959 |            else convertError loc env (NApp xfc (NLocal xr x xp) [])
  960 |                                      (NApp yfc (NLocal yr y yp) [])
  961 |   -- Locally bound things, in a term (not LHS). Since we have to unify
  962 |   -- for *all* possible values, we can safely unify the arguments.
  963 |   unifyBothApps mode@(MkUnifyInfo p InTerm) loc env xfc (NLocal xr x xp) xargs yfc (NLocal yr y yp) yargs
  964 |       = if x == y
  965 |            then unifyArgs mode loc env (map snd xargs) (map snd yargs)
  966 |            else postpone loc mode "Postponing local app"
  967 |                          env (NApp xfc (NLocal xr x xp) xargs)
  968 |                              (NApp yfc (NLocal yr y yp) yargs)
  969 |   unifyBothApps mode loc env xfc (NLocal xr x xp) xargs yfc (NLocal yr y yp) yargs
  970 |       = do log "unify.application" 10 $ "Both local apps, unifyIfEq"
  971 |            unifyIfEq True loc mode env (NApp xfc (NLocal xr x xp) xargs)
  972 |                                        (NApp yfc (NLocal yr y yp) yargs)
  973 |   -- If they're both holes, solve the one with the bigger context
  974 |   unifyBothApps mode loc env xfc (NMeta xn xi xargs) xargs' yfc (NMeta yn yi yargs) yargs'
  975 |       = do invx <- isDefInvertible loc xi
  976 |            if xi == yi && (invx || umode mode == InSearch)
  977 |                                -- Invertible, (from auto implicit search)
  978 |                                -- so we can also unify the arguments.
  979 |               then unifyArgs mode loc env (xargs ++ map snd xargs')
  980 |                                           (yargs ++ map snd yargs')
  981 |               else do xlocs <- localsIn xargs
  982 |                       ylocs <- localsIn yargs
  983 |                       -- Solve the one with the bigger context, and if they're
  984 |                       -- equal, the one that's applied to fewest things (because
  985 |                       -- then they arguments get substituted in)
  986 |                       let xbigger = xlocs > ylocs
  987 |                                       || (xlocs == ylocs &&
  988 |                                            length xargs' <= length yargs')
  989 |                       if (xbigger || umode mode == InMatch) && not (pv xn)
  990 |                         then unifyApp False mode loc env xfc (NMeta xn xi xargs) xargs'
  991 |                                             (NApp yfc (NMeta yn yi yargs) yargs')
  992 |                         else unifyApp True mode loc env yfc (NMeta yn yi yargs) yargs'
  993 |                                            (NApp xfc (NMeta xn xi xargs) xargs')
  994 |     where
  995 |       pv : Name -> Bool
  996 |       pv (PV {}) = True
  997 |       pv _ = False
  998 | 
  999 |       localsIn : List (Closure vars) -> Core Nat
 1000 |       localsIn [] = pure 0
 1001 |       localsIn (c :: cs)
 1002 |           = do defs <- get Ctxt
 1003 |                case !(evalClosure defs c) of
 1004 |                  NApp _ (NLocal {}) _ => pure $ S !(localsIn cs)
 1005 |                  _ => localsIn cs
 1006 | 
 1007 |   unifyBothApps mode loc env xfc (NMeta xn xi xargs) xargs' yfc fy yargs'
 1008 |       = unifyApp False mode loc env xfc (NMeta xn xi xargs) xargs'
 1009 |                                         (NApp yfc fy yargs')
 1010 |   unifyBothApps mode loc env xfc fx xargs' yfc (NMeta yn yi yargs) yargs'
 1011 |       = if umode mode /= InMatch
 1012 |            then unifyApp True mode loc env xfc (NMeta yn yi yargs) yargs'
 1013 |                                                (NApp xfc fx xargs')
 1014 |            else unifyApp False mode loc env xfc fx xargs'
 1015 |                                         (NApp yfc (NMeta yn yi yargs) yargs')
 1016 |   unifyBothApps mode@(MkUnifyInfo p InSearch) loc env xfc fx@(NRef xt hdx) xargs yfc fy@(NRef yt hdy) yargs
 1017 |       = if hdx == hdy
 1018 |            then unifyArgs mode loc env (map snd xargs) (map snd yargs)
 1019 |            else unifyApp False mode loc env xfc fx xargs (NApp yfc fy yargs)
 1020 |   unifyBothApps mode@(MkUnifyInfo p InMatch) loc env xfc fx@(NRef xt hdx) xargs yfc fy@(NRef yt hdy) yargs
 1021 |       = if hdx == hdy
 1022 |            then do logC "unify.application" 5
 1023 |                           (do defs <- get Ctxt
 1024 |                               xs <- traverse (quote defs env) (map snd xargs)
 1025 |                               ys <- traverse (quote defs env) (map snd yargs)
 1026 |                               pure ("Matching args " ++ show xs ++ " " ++ show ys))
 1027 |                    unifyArgs mode loc env (map snd xargs) (map snd yargs)
 1028 |            else unifyApp False mode loc env xfc fx xargs (NApp yfc fy yargs)
 1029 |   unifyBothApps mode loc env xfc fx ax yfc fy ay
 1030 |       = unifyApp False mode loc env xfc fx ax (NApp yfc fy ay)
 1031 | 
 1032 |   unifyPiInfo : {auto c : Ref Ctxt Defs} ->
 1033 |                 {auto u : Ref UST UState} ->
 1034 |                 {vars : _} ->
 1035 |                 UnifyInfo -> FC -> Env Term vars ->
 1036 |                 PiInfo (Closure vars) -> PiInfo (Closure vars) ->
 1037 |                 Core (Maybe UnifyResult)
 1038 |   unifyPiInfo mode loc env Explicit Explicit = pure $ Just success
 1039 |   unifyPiInfo mode loc env Implicit Implicit = pure $ Just success
 1040 |   unifyPiInfo mode loc env AutoImplicit AutoImplicit = pure $ Just success
 1041 |   unifyPiInfo mode loc env (DefImplicit x) (DefImplicit y) = Just <$> unify mode loc env x y
 1042 |   unifyPiInfo mode loc env _ _ = pure Nothing
 1043 | 
 1044 |   unifyBothBinders: {auto c : Ref Ctxt Defs} ->
 1045 |                     {auto u : Ref UST UState} ->
 1046 |                     {vars : _} ->
 1047 |                     UnifyInfo -> FC -> Env Term vars ->
 1048 |                     FC -> Name -> Binder (Closure vars) ->
 1049 |                     (Defs -> Closure vars -> Core (NF vars)) ->
 1050 |                     FC -> Name -> Binder (Closure vars) ->
 1051 |                     (Defs -> Closure vars -> Core (NF vars)) ->
 1052 |                     Core UnifyResult
 1053 |   unifyBothBinders mode loc env xfc x (Pi fcx cx ix tx) scx yfc y (Pi fcy cy iy ty) scy
 1054 |       = do defs <- get Ctxt
 1055 |            let err = convertError loc env
 1056 |                        (NBind xfc x (Pi fcx cx ix tx) scx)
 1057 |                        (NBind yfc y (Pi fcy cy iy ty) scy)
 1058 |            if cx /= cy
 1059 |              then err
 1060 |              else do Just ci <- unifyPiInfo (lower mode) loc env ix iy
 1061 |                        | Nothing => err
 1062 |                      empty <- clearDefs defs
 1063 |                      tx' <- quote empty env tx
 1064 |                      logC "unify.binder" 10 $
 1065 |                                (do ty' <- quote empty env ty
 1066 |                                    pure ("Unifying arg types " ++ show tx' ++ " and " ++ show ty'))
 1067 |                      ct <- unify (lower mode) loc env tx ty
 1068 |                      xn <- genVarName "x"
 1069 |                      let env' : Env Term (x :: _)
 1070 |                               = Pi fcy cy Explicit tx' :: env
 1071 |                      case constraints ct of
 1072 |                          [] => -- No constraints, check the scope
 1073 |                             do tscx <- scx defs (toClosure defaultOpts env (Ref loc Bound xn))
 1074 |                                tscy <- scy defs (toClosure defaultOpts env (Ref loc Bound xn))
 1075 |                                tmx <- quote empty env tscx
 1076 |                                tmy <- quote empty env tscy
 1077 |                                cs <- unify (lower mode) loc env'
 1078 |                                        (refsToLocals (Add x xn None) tmx)
 1079 |                                        (refsToLocals (Add x xn None) tmy)
 1080 |                                pure (union ci cs)
 1081 |                          cs => -- Constraints, make new guarded constant
 1082 |                             do txtm <- quote empty env tx
 1083 |                                tytm <- quote empty env ty
 1084 |                                c <- newConstant loc erased env
 1085 |                                       (Bind xfc x (Lam fcy cy Explicit txtm) (Local xfc Nothing _ First))
 1086 |                                       (Bind xfc x (Pi fcy cy Explicit txtm)
 1087 |                                           (weaken tytm)) cs
 1088 |                                tscx <- scx defs (toClosure defaultOpts env (Ref loc Bound xn))
 1089 |                                tscy <- scy defs (toClosure defaultOpts env (App loc c (Ref loc Bound xn)))
 1090 |                                tmx <- quote empty env tscx
 1091 |                                tmy <- quote empty env tscy
 1092 |                                cs' <- unify (lower mode) loc env'
 1093 |                                         (refsToLocals (Add x xn None) tmx)
 1094 |                                         (refsToLocals (Add x xn None) tmy)
 1095 |                                pure (union ci (union ct cs'))
 1096 |   unifyBothBinders mode loc env xfc x (Lam fcx cx ix tx) scx yfc y (Lam fcy cy iy ty) scy
 1097 |       = do defs <- get Ctxt
 1098 |            let err = convertError loc env
 1099 |                        (NBind xfc x (Lam fcx cx ix tx) scx)
 1100 |                        (NBind yfc y (Lam fcy cy iy ty) scy)
 1101 |            if cx /= cy
 1102 |              then err
 1103 |              else do empty <- clearDefs defs
 1104 |                      Just ci <- unifyPiInfo (lower mode) loc env ix iy
 1105 |                        | Nothing => err
 1106 |                      ct <- unify (lower mode) loc env tx ty
 1107 |                      xn <- genVarName "x"
 1108 |                      txtm <- quote empty env tx
 1109 |                      let env' : Env Term (x :: _)
 1110 |                               = Lam fcx cx Explicit txtm :: env
 1111 | 
 1112 |                      tscx <- scx defs (toClosure defaultOpts env (Ref loc Bound xn))
 1113 |                      tscy <- scy defs (toClosure defaultOpts env (Ref loc Bound xn))
 1114 |                      tmx <- quote empty env tscx
 1115 |                      tmy <- quote empty env tscy
 1116 |                      cs' <- unify (lower mode) loc env' (refsToLocals (Add x xn None) tmx)
 1117 |                                                               (refsToLocals (Add x xn None) tmy)
 1118 |                      pure (union ci (union ct cs'))
 1119 | 
 1120 |   unifyBothBinders mode loc env xfc x bx scx yfc y by scy
 1121 |       = convertError loc env
 1122 |                   (NBind xfc x bx scx)
 1123 |                   (NBind yfc y by scy)
 1124 | 
 1125 |   dumpArg : {vars : _} ->
 1126 |             {auto c : Ref Ctxt Defs} ->
 1127 |             Env Term vars -> Closure vars -> Core ()
 1128 |   dumpArg env (MkClosure opts loc lenv tm)
 1129 |       = do defs <- get Ctxt
 1130 |            empty <- clearDefs defs
 1131 |            logTerm "unify" 20 "Term: " tm
 1132 |            nf <- evalClosure empty (MkClosure opts loc lenv tm)
 1133 |            logNF "unify" 20 "  " env nf
 1134 |   dumpArg env cl
 1135 |       = do defs <- get Ctxt
 1136 |            empty <- clearDefs defs
 1137 |            nf <- evalClosure empty cl
 1138 |            logNF "unify" 20 "  " env nf
 1139 | 
 1140 |   export
 1141 |   unifyNoEta : {auto c : Ref Ctxt Defs} ->
 1142 |                {auto u : Ref UST UState} ->
 1143 |                {vars : _} ->
 1144 |                UnifyInfo -> FC -> Env Term vars ->
 1145 |                NF vars -> NF vars ->
 1146 |                Core UnifyResult
 1147 |   unifyNoEta mode loc env (NDCon xfc x tagx ax xs) (NDCon yfc y tagy ay ys)
 1148 |       = do gam <- get Ctxt
 1149 |            if tagx == tagy
 1150 |              then
 1151 |                   do -- Constantly checking the log setting appears to have
 1152 |                      -- a bit of overhead, but I'm keeping this here because it
 1153 |                      -- may prove useful again...
 1154 |                      {-
 1155 |                      ust <- get UST
 1156 |                      when (logging ust) $
 1157 |                         do logC "unify" 20 $ do pure $ "Constructor " ++ show !(toFullNames x) ++ " " ++ show loc
 1158 |                            log "unify" 20 "ARGUMENTS:"
 1159 |                            traverse_ (dumpArg env) xs
 1160 |                            log "unify" 20 "WITH:"
 1161 |                            traverse_ (dumpArg env) ys
 1162 |                      -}
 1163 |                      unifyArgs mode loc env (map snd xs) (map snd ys)
 1164 |              else convertError loc env
 1165 |                        (NDCon xfc x tagx ax xs)
 1166 |                        (NDCon yfc y tagy ay ys)
 1167 |   unifyNoEta mode loc env (NTCon xfc x ax xs) (NTCon yfc y ay ys)
 1168 |    = do logC "unify" 20 $ do
 1169 |           x <- toFullNames x
 1170 |           y <- toFullNames y
 1171 |           pure $ "Comparing type constructors " ++ show x ++ " and " ++ show y
 1172 |         if x == y
 1173 |            then do let xs = map snd xs
 1174 |                    let ys = map snd ys
 1175 | 
 1176 |                    logC "unify" 20 $
 1177 |                      pure $ "Constructor " ++ show x
 1178 |                    logC "unify" 20 $ map (const "") $ traverse_ (dumpArg env) xs
 1179 |                    logC "unify" 20 $ map (const "") $ traverse_ (dumpArg env) ys
 1180 |                    unifyArgs mode loc env xs ys
 1181 |              -- TODO: Type constructors are not necessarily injective.
 1182 |              -- If we don't know it's injective, need to postpone the
 1183 |              -- constraint. But before then, we need some way to decide
 1184 |              -- what's injective...
 1185 |              -- gallais: really? We don't mind being anticlassical do we?
 1186 | --                then postpone True loc mode env (quote empty env (NTCon x ax xs))
 1187 | --                                           (quote empty env (NTCon y ay ys))
 1188 |            else convertError loc env
 1189 |                      (NTCon xfc x ax xs)
 1190 |                      (NTCon yfc y ay ys)
 1191 |   unifyNoEta mode loc env (NDelayed xfc _ x) (NDelayed yfc _ y)
 1192 |       = unify (lower mode) loc env x y
 1193 |   unifyNoEta mode loc env (NDelay xfc _ xty x) (NDelay yfc _ yty y)
 1194 |       = unifyArgs mode loc env [xty, x] [yty, y]
 1195 |   unifyNoEta mode loc env (NForce xfc _ x axs) (NForce yfc _ y ays)
 1196 |       = do cs <- unify (lower mode) loc env x y
 1197 |            cs' <- unifyArgs mode loc env (map snd axs) (map snd ays)
 1198 |            pure (union cs cs')
 1199 |   unifyNoEta mode loc env x@(NApp xfc fx@(NMeta {}) axs)
 1200 |                           y@(NApp yfc fy@(NMeta {}) ays)
 1201 |       = do defs <- get Ctxt
 1202 |            if !(convert defs env x y)
 1203 |                then pure success
 1204 |                else unifyBothApps (lower mode) loc env xfc fx axs yfc fy ays
 1205 |   unifyNoEta mode loc env (NApp xfc fx axs) (NApp yfc fy ays)
 1206 |       = unifyBothApps (lower mode) loc env xfc fx axs yfc fy ays
 1207 |   unifyNoEta mode loc env x (NErased _ (Dotted y)) = unifyNoEta mode loc env x y
 1208 |   unifyNoEta mode loc env (NErased _ (Dotted x)) y = unifyNoEta mode loc env x y
 1209 |   unifyNoEta mode loc env (NApp xfc hd args) y
 1210 |       = unifyApp False (lower mode) loc env xfc hd args y
 1211 |   unifyNoEta mode loc env y (NApp yfc hd args)
 1212 |       = if umode mode /= InMatch
 1213 |            then unifyApp True mode loc env yfc hd args y
 1214 |            else do log "unify.noeta" 10 $ "Unify if Eq due to something with app"
 1215 |                    unifyIfEq True loc mode env y (NApp yfc hd args)
 1216 |   -- Only try stripping as patterns as a last resort
 1217 |   unifyNoEta mode loc env x (NAs _ _ _ y) = unifyNoEta mode loc env x y
 1218 |   unifyNoEta mode loc env (NAs _ _ _ x) y = unifyNoEta mode loc env x y
 1219 |   unifyNoEta mode loc env x y
 1220 |       = do defs <- get Ctxt
 1221 |            empty <- clearDefs defs
 1222 |            log "unify.noeta" 10 $ "Nothing else worked, unifyIfEq"
 1223 |            unifyIfEq (isDelay x || isDelay y) loc mode env x y
 1224 |     where
 1225 |       -- If one of them is a delay, and they're not equal, we'd better
 1226 |       -- postpone and come back to it so we can insert the implicit
 1227 |       -- Force/Delay later
 1228 |       isDelay : NF vars -> Bool
 1229 |       isDelay (NDelayed {}) = True
 1230 |       isDelay _ = False
 1231 | 
 1232 |   isHoleApp : NF vars -> Bool
 1233 |   isHoleApp (NApp _ (NMeta {}) _) = True
 1234 |   isHoleApp _ = False
 1235 | 
 1236 |   export
 1237 |   Unify NF where
 1238 |     unifyD _ _ mode loc env (NBind xfc x bx scx) (NBind yfc y by scy)
 1239 |         = unifyBothBinders mode loc env xfc x bx scx yfc y by scy
 1240 |     unifyD _ _ mode loc env tmx@(NBind xfc x (Lam fcx cx ix tx) scx) tmy
 1241 |         = do defs <- get Ctxt
 1242 |              logNF "unify" 10 "EtaR" env tmx
 1243 |              logNF "unify" 10 "...with" env tmy
 1244 |              if isHoleApp tmy
 1245 |                 then if not !(convert defs env tmx tmy)
 1246 |                         then unifyNoEta (lower mode) loc env tmx tmy
 1247 |                         else pure success
 1248 |                 else do empty <- clearDefs defs
 1249 |                         domty <- quote empty env tx
 1250 |                         etay <- nf defs env
 1251 |                                   $ Bind xfc x (Lam fcx cx Explicit domty)
 1252 |                                   $ App xfc (weaken !(quote empty env tmy))
 1253 |                                             (Local xfc Nothing 0 First)
 1254 |                         logNF "unify" 10 "Expand" env etay
 1255 |                         unify (lower mode) loc env tmx etay
 1256 |     unifyD _ _ mode loc env tmx tmy@(NBind yfc y (Lam fcy cy iy ty) scy)
 1257 |         = do defs <- get Ctxt
 1258 |              logNF "unify" 10 "EtaL" env tmx
 1259 |              logNF "unify" 10 "...with" env tmy
 1260 |              if isHoleApp tmx
 1261 |                 then if not !(convert defs env tmx tmy)
 1262 |                         then unifyNoEta (lower mode) loc env tmx tmy
 1263 |                         else pure success
 1264 |                 else do empty <- clearDefs defs
 1265 |                         domty <- quote empty env ty
 1266 |                         etax <- nf defs env
 1267 |                                  $ Bind yfc y (Lam fcy cy Explicit domty)
 1268 |                                  $ App yfc (weaken !(quote empty env tmx))
 1269 |                                            (Local yfc Nothing 0 First)
 1270 |                         logNF "unify" 10 "Expand" env etax
 1271 |                         unify (lower mode) loc env etax tmy
 1272 |     unifyD _ _ mode loc env tmx tmy = unifyNoEta mode loc env tmx tmy
 1273 | 
 1274 |     unifyWithLazyD _ _ mode loc env (NDelayed _ _ tmx) (NDelayed _ _ tmy)
 1275 |        = unify (lower mode) loc env tmx tmy
 1276 |     unifyWithLazyD _ _ mode loc env x@(NDelayed _ r tmx) tmy
 1277 |        = if isHoleApp tmy && not (umode mode == InMatch)
 1278 |             -- given type delayed, expected unknown, so let's wait and see
 1279 |             -- what the expected type turns out to be
 1280 |             then postpone loc mode "Postponing in lazy" env x tmy
 1281 |             else do vs <- unify (lower mode) loc env tmx tmy
 1282 |                     pure ({ addLazy := AddForce r } vs)
 1283 |     unifyWithLazyD _ _ mode loc env tmx (NDelayed _ r tmy)
 1284 |        = do vs <- unify (lower mode) loc env tmx tmy
 1285 |             pure ({ addLazy := AddDelay r } vs)
 1286 |     unifyWithLazyD _ _ mode loc env tmx tmy
 1287 |        = unify mode loc env tmx tmy
 1288 | 
 1289 |   export
 1290 |   Unify Term where
 1291 |     unifyD _ _ mode loc env x y
 1292 |           = do defs <- get Ctxt
 1293 |                empty <- clearDefs defs
 1294 |                if x == y
 1295 |                   then do log "unify.equal" 10 $
 1296 |                                  "Skipped unification (equal already): "
 1297 |                                  ++ show x ++ " and " ++ show y
 1298 |                           pure success
 1299 |                   else do xnf <- nf defs env x
 1300 |                           ynf <- nf defs env y
 1301 |                           unify mode loc env xnf ynf
 1302 |     unifyWithLazyD _ _ mode loc env x y
 1303 |           = do defs <- get Ctxt
 1304 |                empty <- clearDefs defs
 1305 |                if x == y
 1306 |                   then do log "unify.equal" 10 $
 1307 |                                  "Skipped unification (equal already): "
 1308 |                                  ++ show x ++ " and " ++ show y
 1309 |                           pure success
 1310 |                   else do xnf <- nf defs env x
 1311 |                           ynf <- nf defs env y
 1312 |                           unifyWithLazy mode loc env xnf ynf
 1313 | 
 1314 |   export
 1315 |   Unify Closure where
 1316 |     unifyD _ _ mode loc env x y
 1317 |         = do defs <- get Ctxt
 1318 |              empty <- clearDefs defs
 1319 |              if !(convert empty env x y)
 1320 |                 then pure success
 1321 |                 else
 1322 |                   do xnf <- evalClosure defs x
 1323 |                      ynf <- evalClosure defs y
 1324 |                      -- If one's a meta and the other isn't, don't reduce at
 1325 |                      -- all
 1326 |                      case (xnf, ynf) of
 1327 |                          -- They might be equal, don't want to make a cycle
 1328 |                          (NApp _ (NMeta {}) _, NApp _ (NMeta {}) _)
 1329 |                                => unify mode loc env xnf ynf
 1330 |                          (NApp _ (NMeta _ i _) _, _) =>
 1331 |                             do ynf' <- evalClosure empty y
 1332 |                                xtm <- quote empty env xnf
 1333 |                                ytm <- quote empty env ynf'
 1334 |                                cs <- unify mode loc env !(nf empty env xtm)
 1335 |                                                         !(nf empty env ytm)
 1336 |                                case constraints cs of
 1337 |                                     [] => pure cs
 1338 |                                     _ => do ynf <- evalClosure defs y
 1339 |                                             unify mode loc env xnf ynf
 1340 |                          (_, NApp _ (NMeta _ i _ ) _) =>
 1341 |                             do xnf' <- evalClosure empty x
 1342 |                                xtm <- quote empty env xnf'
 1343 |                                ytm <- quote empty env ynf
 1344 |                                cs <- unify mode loc env !(nf empty env ytm)
 1345 |                                                         !(nf empty env xtm)
 1346 |                                case constraints cs of
 1347 |                                     [] => pure cs
 1348 |                                     _ => unify mode loc env xnf ynf
 1349 |                          _ => unify mode loc env xnf ynf
 1350 | 
 1351 | export
 1352 | setInvertible : {auto c : Ref Ctxt Defs} ->
 1353 |                 FC -> Name -> Core ()
 1354 | setInvertible fc n
 1355 |     = do defs <- get Ctxt
 1356 |          Just gdef <- lookupCtxtExact n (gamma defs)
 1357 |               | Nothing => undefinedName fc n
 1358 |          ignore $ addDef n ({ invertible := True } gdef)
 1359 | 
 1360 | public export
 1361 | data SolveMode = Normal -- during elaboration: unifies and searches
 1362 |                | Defaults -- unifies and searches for default hints only
 1363 |                | MatchArgs -- match rather than unify
 1364 |                | LastChance -- as normal, but any failure throws rather than delays
 1365 | 
 1366 | Eq SolveMode where
 1367 |   Normal == Normal = True
 1368 |   Defaults == Defaults = True
 1369 |   LastChance == LastChance = True
 1370 |   _ == _ = False
 1371 | 
 1372 | 
 1373 | retry : {auto c : Ref Ctxt Defs} ->
 1374 |         {auto u : Ref UST UState} ->
 1375 |         UnifyInfo -> Int -> Core UnifyResult
 1376 | retry mode c
 1377 |     = do ust <- get UST
 1378 |          case lookup c (constraints ust) of
 1379 |               Nothing => pure success
 1380 |               Just Resolved => pure success
 1381 |               Just (MkConstraint loc withLazy env xold yold)
 1382 |                => do defs <- get Ctxt
 1383 |                      x <- continueNF defs env xold
 1384 |                      y <- continueNF defs env yold
 1385 |                      catch
 1386 |                        (do logNF "unify.retry" 5 ("Retrying " ++ show c ++ " " ++ show (umode mode)) env x
 1387 |                            logNF "unify.retry" 5 "....with" env y
 1388 |                            log "unify.retry" 5 $ if withLazy
 1389 |                                       then "(lazy allowed)"
 1390 |                                       else "(no lazy)"
 1391 |                            cs <- ifThenElse withLazy
 1392 |                                     (unifyWithLazy mode loc env x y)
 1393 |                                     (unify (lower mode) loc env x y)
 1394 |                            case constraints cs of
 1395 |                              [] => do log "unify.retry" 5 $ "Success " ++ show (addLazy cs)
 1396 |                                       deleteConstraint c
 1397 |                                       pure cs
 1398 |                              _ => do log "unify.retry" 5 $ "Constraints " ++ show (addLazy cs)
 1399 |                                      pure cs)
 1400 |                       (\err => do defs <- get Ctxt
 1401 |                                   empty <- clearDefs defs
 1402 |                                   throw (WhenUnifying loc (gamma defs) env !(quote empty env x) !(quote empty env y) err))
 1403 | 
 1404 | delayMeta : {vars : _} ->
 1405 |             LazyReason -> Nat -> Term vars -> Term vars -> Term vars
 1406 | delayMeta r (S k) ty (Bind fc n b sc)
 1407 |     = Bind fc n b (delayMeta r k (weaken ty) sc)
 1408 | delayMeta r envb ty tm = TDelay (getLoc tm) r ty tm
 1409 | 
 1410 | forceMeta : LazyReason -> Nat -> Term vars -> Term vars
 1411 | forceMeta r (S k) (Bind fc n b sc)
 1412 |     = Bind fc n b (forceMeta r k sc)
 1413 | forceMeta r envb tm = TForce (getLoc tm) r tm
 1414 | 
 1415 | -- Check whether it's worth trying a search again, based on what went wrong
 1416 | recoverable : Error -> Bool
 1417 | recoverable (UndefinedName {}) = False
 1418 | recoverable (InType _ _ err) = recoverable err
 1419 | recoverable (InCon _ err) = recoverable err
 1420 | recoverable (InLHS _ _ err) = recoverable err
 1421 | recoverable (InRHS _ _ err) = recoverable err
 1422 | recoverable (WhenUnifying _ _ _ _ _ err) = recoverable err
 1423 | recoverable (MaybeMisspelling err _) = recoverable err
 1424 | recoverable _ = True
 1425 | 
 1426 | -- Retry the given constraint, return True if progress was made
 1427 | retryGuess : {auto c : Ref Ctxt Defs} ->
 1428 |              {auto u : Ref UST UState} ->
 1429 |              UnifyInfo -> (smode : SolveMode) -> (hole : (Int, (FC, Name))) ->
 1430 |              Core Bool
 1431 | retryGuess mode smode (hid, (loc, hname))
 1432 |     = do defs <- get Ctxt
 1433 |          case !(lookupCtxtExact (Resolved hid) (gamma defs)) of
 1434 |            Nothing => pure False
 1435 |            Just def =>
 1436 |              case definition def of
 1437 |                BySearch rig depth defining =>
 1438 |                   handleUnify
 1439 |                      (do tm <- search loc rig (smode == Defaults) depth defining
 1440 |                                       (type def) Env.empty
 1441 |                          let gdef = { definition := PMDef defaultPI Scope.empty (STerm 0 tm) (STerm 0 tm) [] } def
 1442 |                          logTermNF "unify.retry" 5 ("Solved " ++ show hname) Env.empty tm
 1443 |                          ignore $ addDef (Resolved hid) gdef
 1444 |                          removeGuess hid
 1445 |                          pure True)
 1446 |                      $ \case
 1447 |                        DeterminingArg _ n i _ _ =>
 1448 |                          do logTerm "unify.retry" 5
 1449 |                                     ("Failed (det " ++ show hname ++ " " ++ show n ++ ")")
 1450 |                                     (type def)
 1451 |                             setInvertible loc (Resolved i)
 1452 |                             pure False -- progress not made yet!
 1453 |                        err =>
 1454 |                          do logTermNF "unify.retry" 5
 1455 |                                       ("Search failed at " ++ show rig ++ " for " ++ show hname)
 1456 |                                       Env.empty (type def)
 1457 |                             case smode of
 1458 |                                  LastChance => throw err
 1459 |                                  _ => if recoverable err
 1460 |                                          then pure False -- Postpone again
 1461 |                                          else throw (CantSolveGoal loc (gamma defs)
 1462 |                                                         Env.empty (type def) (Just err))
 1463 |                Guess tm envb [constr] =>
 1464 |                  do let umode = case smode of
 1465 |                                      MatchArgs => inMatch
 1466 |                                      _ => mode
 1467 |                     cs <- retry umode constr
 1468 |                     case constraints cs of
 1469 |                          [] => do tm' <- case addLazy cs of
 1470 |                                            NoLazy => pure tm
 1471 |                                            AddForce r => pure $ forceMeta r envb tm
 1472 |                                            AddDelay r =>
 1473 |                                               do ty <- getType Env.empty tm
 1474 |                                                  logTerm "unify.retry" 5 "Retry Delay" tm
 1475 |                                                  pure $ delayMeta r envb !(getTerm ty) tm
 1476 |                                   let gdef = { definition := PMDef (MkPMDefInfo NotHole True False)
 1477 |                                                                    Scope.empty (STerm 0 tm') (STerm 0 tm') [] } def
 1478 |                                   logTerm "unify.retry" 5 ("Resolved " ++ show hname) tm'
 1479 |                                   ignore $ addDef (Resolved hid) gdef
 1480 |                                   removeGuess hid
 1481 |                                   pure (holesSolved cs)
 1482 |                          newcs => do tm' <- case addLazy cs of
 1483 |                                            NoLazy => pure tm
 1484 |                                            AddForce r => pure $ forceMeta r envb tm
 1485 |                                            AddDelay r =>
 1486 |                                               do ty <- getType Env.empty tm
 1487 |                                                  logTerm "unify.retry" 5 "Retry Delay (constrained)" tm
 1488 |                                                  pure $ delayMeta r envb !(getTerm ty) tm
 1489 |                                      let gdef = { definition := Guess tm' envb newcs } def
 1490 |                                      ignore $ addDef (Resolved hid) gdef
 1491 |                                      pure False
 1492 |                Guess tm envb constrs =>
 1493 |                  do let umode = case smode of
 1494 |                                      MatchArgs => inMatch
 1495 |                                      _ => mode
 1496 |                     cs' <- traverse (retry umode) constrs
 1497 |                     let csAll = unionAll cs'
 1498 |                     case constraints csAll of
 1499 |                          -- All constraints resolved, so turn into a
 1500 |                          -- proper definition and remove it from the
 1501 |                          -- hole list
 1502 |                          [] => do let gdef = { definition := PMDef (MkPMDefInfo NotHole True False)
 1503 |                                                                    Scope.empty (STerm 0 tm) (STerm 0 tm) [] } def
 1504 |                                   logTerm "unify.retry" 5 ("Resolved " ++ show hname) tm
 1505 |                                   ignore $ addDef (Resolved hid) gdef
 1506 |                                   removeGuess hid
 1507 |                                   pure (holesSolved csAll)
 1508 |                          newcs => do let gdef = { definition := Guess tm envb newcs } def
 1509 |                                      ignore $ addDef (Resolved hid) gdef
 1510 |                                      pure False
 1511 |                _ => pure False
 1512 | 
 1513 | export
 1514 | solveConstraints : {auto c : Ref Ctxt Defs} ->
 1515 |                    {auto u : Ref UST UState} ->
 1516 |                    UnifyInfo -> (smode : SolveMode) -> Core ()
 1517 | solveConstraints umode smode
 1518 |     = do ust <- get UST
 1519 |          progress <- traverse (retryGuess umode smode) (toList (guesses ust))
 1520 |          when (any id progress) $
 1521 |                solveConstraints umode Normal
 1522 | 
 1523 | export
 1524 | solveConstraintsAfter : {auto c : Ref Ctxt Defs} ->
 1525 |                         {auto u : Ref UST UState} ->
 1526 |                         Int -> UnifyInfo -> (smode : SolveMode) -> Core ()
 1527 | solveConstraintsAfter start umode smode
 1528 |     = do ust <- get UST
 1529 |          progress <- traverse (retryGuess umode smode)
 1530 |                               (filter afterStart (toList (guesses ust)))
 1531 |          when (any id progress) $
 1532 |                solveConstraintsAfter start umode Normal
 1533 |   where
 1534 |     afterStart : (Int, a) -> Bool
 1535 |     afterStart (x, _) = x >= start
 1536 | 
 1537 | -- Replace any 'BySearch' with 'Hole', so that we don't keep searching
 1538 | -- fruitlessly while elaborating the rest of a source file
 1539 | export
 1540 | giveUpConstraints : {auto c : Ref Ctxt Defs} ->
 1541 |                     {auto u : Ref UST UState} ->
 1542 |                     Core ()
 1543 | giveUpConstraints
 1544 |     = do ust <- get UST
 1545 |          traverse_ constraintToHole (toList (guesses ust))
 1546 |   where
 1547 |     constraintToHole : (Int, (FC, Name)) -> Core ()
 1548 |     constraintToHole (hid, (_, _))
 1549 |         = do defs <- get Ctxt
 1550 |              case !(lookupDefExact (Resolved hid) (gamma defs)) of
 1551 |                   Just (BySearch {}) =>
 1552 |                          updateDef (Resolved hid) (const (Just (Hole 0 (holeInit False))))
 1553 |                   Just (Guess {}) =>
 1554 |                          updateDef (Resolved hid) (const (Just (Hole 0 (holeInit False))))
 1555 |                   _ => pure ()
 1556 | 
 1557 | -- Check whether any of the given hole references have the same solution
 1558 | -- (up to conversion)
 1559 | export
 1560 | checkArgsSame : {auto u : Ref UST UState} ->
 1561 |                 {auto c : Ref Ctxt Defs} ->
 1562 |                 List Int -> Core Bool
 1563 | checkArgsSame [] = pure False
 1564 | checkArgsSame (x :: xs)
 1565 |     = do defs <- get Ctxt
 1566 |          Just (PMDef _ [] (STerm 0 def) _ _) <-
 1567 |                     lookupDefExact (Resolved x) (gamma defs)
 1568 |               | _ => checkArgsSame xs
 1569 |          s <- anySame def xs
 1570 |          if s
 1571 |             then pure True
 1572 |             else checkArgsSame xs
 1573 |   where
 1574 |     anySame : ClosedTerm -> List Int -> Core Bool
 1575 |     anySame tm [] = pure False
 1576 |     anySame tm (t :: ts)
 1577 |         = do defs <- get Ctxt
 1578 |              Just (PMDef _ [] (STerm 0 def) _ _) <-
 1579 |                         lookupDefExact (Resolved t) (gamma defs)
 1580 |                  | _ => anySame tm ts
 1581 |              if !(convert defs Env.empty tm def)
 1582 |                 then pure True
 1583 |                 else anySame tm ts
 1584 | 
 1585 | export
 1586 | checkDots : {auto u : Ref UST UState} ->
 1587 |             {auto c : Ref Ctxt Defs} ->
 1588 |             Core ()
 1589 | checkDots
 1590 |     = do ust <- get UST
 1591 |          hs <- getCurrentHoles
 1592 |          traverse_ checkConstraint (reverse (dotConstraints ust))
 1593 |          hs <- getCurrentHoles
 1594 |          update UST { dotConstraints := [] }
 1595 |   where
 1596 |     getHoleName : ClosedTerm -> Core (Maybe Name)
 1597 |     getHoleName tm
 1598 |         = do defs <- get Ctxt
 1599 |              NApp _ (NMeta n' i args) _ <- nf defs Env.empty tm
 1600 |                  | _ => pure Nothing
 1601 |              pure (Just n')
 1602 | 
 1603 |     checkConstraint : (Name, DotReason, Constraint) -> Core ()
 1604 |     checkConstraint (n, reason, MkConstraint fc wl env xold yold)
 1605 |         = do defs <- get Ctxt
 1606 |              x <- continueNF defs env xold
 1607 |              y <- continueNF defs env yold
 1608 |              logNF "unify.constraint" 10 "Dot" env y
 1609 |              logNF "unify.constraint" 10 "  =" env x
 1610 |              -- A dot is okay if the constraint is solvable *without solving
 1611 |              -- any additional holes*
 1612 |              ust <- get UST
 1613 |              handleUnify
 1614 |                (do defs <- get Ctxt
 1615 |                    -- get the hole name that 'n' is currently resolved to,
 1616 |                    -- if indeed it is still a hole
 1617 |                    (i, _) <- getPosition n (gamma defs)
 1618 |                    oldholen <- getHoleName (Meta fc n i [])
 1619 | 
 1620 |                    -- Check that what was given (x) matches what was
 1621 |                    -- solved by unification (y).
 1622 |                    -- In 'InMatch' mode, only metavariables in 'x' can
 1623 |                    -- be solved, so everything in the dotted metavariable
 1624 |                    -- must be complete.
 1625 |                    cs <- unify inMatch fc env x y
 1626 |                    defs <- get Ctxt
 1627 | 
 1628 |                    -- If the name standing for the dot wasn't solved
 1629 |                    -- earlier, but is now (even with another metavariable)
 1630 |                    -- this is bad (it most likely means there's a non-linear
 1631 |                    -- variable)
 1632 |                    dotSolved <-
 1633 |                       maybe (pure False)
 1634 |                             (\n => do Just ndef <- lookupDefExact n (gamma defs)
 1635 |                                            | Nothing => undefinedName fc n
 1636 |                                       pure $ case ndef of
 1637 |                                            Hole {} => False
 1638 |                                            _ => True)
 1639 |                             oldholen
 1640 | 
 1641 |                    -- If any of the things we solved have the same definition,
 1642 |                    -- we've sneaked a non-linear pattern variable in
 1643 |                    argsSame <- checkArgsSame (namesSolved cs)
 1644 |                    when (not (isNil (constraints cs))
 1645 |                             || dotSolved || argsSame) $
 1646 |                       throw (InternalError "Dot pattern match fail"))
 1647 |                (\err =>
 1648 |                     case err of
 1649 |                          InternalError _ =>
 1650 |                            do defs <- get Ctxt
 1651 |                               Just dty <- lookupTyExact n (gamma defs)
 1652 |                                    | Nothing => undefinedName fc n
 1653 |                               logTermNF "unify.constraint" 5 "Dot type" Env.empty dty
 1654 |                               -- Clear constraints so we don't report again
 1655 |                               -- later
 1656 |                               put UST ({ dotConstraints := [] } ust)
 1657 |                               empty <- clearDefs defs
 1658 |                               throw (BadDotPattern fc env reason
 1659 |                                       !(quote empty env x)
 1660 |                                       !(quote empty env y))
 1661 |                          _ => do put UST ({ dotConstraints := [] } ust)
 1662 |                                  throw err)
 1663 |     checkConstraint _ = pure ()
 1664 |