Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Unification in Idris 2

Unification in Idris 2

Unification concerns type/conversion checking with the presence of meta-variables. Meta-variables are variables with unknown values but type checking/elaboration progress could generate constraints that these variables have to satisfy and thus find the solutions to these variables. Implicits (and implicit arguments) are inferred by unification.

Conversion checking (of terms and closures) determines whether the two inputs are equivalent. Similarly, unification determines whether the two inputs are equivalent with the presence of meta-variables. Naturally, unification is implemented as an extension to conversion checking.

Conversion

Conversion (see Core.Normalise) is extended to support unification. Conversion of Term is normalisation (turn them into normal forms/nf):

Convert Term where
    convGen q defs env x y
        = convGen q defs env !(nf defs env x) !(nf defs env y)

Conversion of Closure is evaluation of closure such that conversion checking can be done:

  Convert Closure where
    convGen q defs env x y
        = convGen q defs env !(evalClosure defs x) !(evalClosure defs y)

The evaluator is pretty standard. To convert binders, we add a new free variable and closure and check that the two evaluated scopes with the new variable added are equal:

convGen q defs env (NBind fc x b sc) (NBind _ x' b' sc')
        = do var <- genName "conv" -- generate a new variable
        --"conv" is a tag for easier debugging
             let c = MkClosure defaultOpts [] env (Ref fc Bound var) -- make a closure with the new variable in it
             bok <- convBinders q defs env b b'
             if bok
                then do bsc <- sc defs c
                        bsc' <- sc' defs c
                        convGen q defs env bsc bsc'
                else pure False

Unification

Unify is similar to conversion except that it maintains a unification state (UState), which keeps track of the meta-variables we are inferring and the constraints we generated for them. See more below.

unify : Unify tm =>
        {vars : _} ->
        {auto c : Ref Ctxt Defs} -> -- the context is required as in conversion
        -- the state stores information of the meta-variables and the their constraints
        {auto u : Ref UST UState} -> 
        UnifyInfo ->
        FC -> Env Term vars ->
        tm vars -> tm vars ->
        Core UnifyResult
unify {c} {u} = unifyD c u

Also, instead of only returning True or False like in conversion, unification returns UnifyResult, which essentially returns:

  • Yes, the terms evaluate to the same thing.
  • No, the terms cannot be evaluated to the same thing and cannot be unified. It throws a type mismatch error.
  • Yes, but..., the terms may be unifiable. No definitive answer on whether the terms can unify or not until there is further progress.

UnifyResult:

record UnifyResult where
  constructor MkUnifyResult
  constraints : List Int
  holesSolved : Bool -- did we solve any holes
  namesSolved : List Int -- which ones did we solve (as name indices)
  addLazy : AddLazy

As we call Unify, some or all of the meta-variables may be solved. These will be stored in the namesSolved field. We may only be able to generate constraints for them. In that case, we don't know whether unification succeed or not until we know the constraints can be satisfied (thus the Yes, but... result).

Holes and guesses

Recall the global context has the following constructors:

data Def : Type where
  Hole : (numlocs : Nat) -> -- Number of locals in scope at binding point
                              -- (mostly to help display)
        HoleFlags ->
        Def
-- Constraints are integer references into the current map of
    -- constraints in the UnifyState (see Core.UnifyState)
  Guess : (guess : ClosedTerm) ->
        (envbind : Nat) -> -- Number of things in the environment when we guessed the term
        (constraints : List Int) -> Def

Any meta-variables we encounter are added to the global context as Hole or Guess. See Type checking in the presence of meta-variables — Ulf Norell, Catarina Coquand, 2007 for details.

A Hole is a meta-variable to be solved. When we encounter a meta-variable, we add them as a Hole in the global context.

A Guess is a meta-variable applied to its current environment. The first argument guess is the value that it should have assuming all the constraints (the third argument) are satisfied. Once the list of constraints becomes an empty list, i.e., constraints = [], The meta-variable can be promoted into an ordinary PMDef in the global context.

The unification state (UState)

UState stores holes and guesses with a global list of constraints, referred to by an Int (or we can use Nat, which is more precise/right):

record UState where
  constructor MkUState
  holes : IntMap (FC, Name) -- All metavariables with no definition yet.
                            -- 'Int' is the 'Resolved' name
  guesses : IntMap (FC, Name) -- Names which will be defined when constraints solved
                              -- (also includes auto implicit searches)
  currentHoles : IntMap (FC, Name) -- Holes introduced this elaboration session
  delayedHoles : IntMap (FC, Name) -- Holes left unsolved after an elaboration,
                                   -- so we need to check again at the end whether
                                   -- they have been solved later. Doesn't include
                                   -- user defined hole names, which don't need
                                   -- to have been solved
  constraints : IntMap Constraint -- map for finding constraints by ID
  dotConstraints : List (Name, DotReason, Constraint) -- dot pattern constraints
  nextName : Int
  nextConstraint : Int
  delayedElab : List (Nat, Int, Core ClosedTerm)
                -- Elaborators which we need to try again later, because
                -- we didn't have enough type information to elaborate
                -- successfully yet.
                -- 'Nat' is the priority (lowest first)
                -- The 'Int' is the resolved name. Delays can't be nested,
                -- so we just process them in order.
  logging : Bool

Generating terms for holes and guesses

newMeta and newConstant are helper functions that create meta-variables.

newMeta (calls newMetaLets) creates a new meta-variable represented by a Hole. Once a new meta-variable is created and unification is applied, one may find a solution for it.

-- Create a new metavariable with the given name and return type,
-- and return a term which is the metavariable applied to the environment
-- (and which has the given type)
-- Flag whether cycles are allowed in the result, and whether to abstract
-- over lets
newMetaLets : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              FC -> RigCount ->
              Env Term vars -> Name -> Term vars -> Def ->
              Bool -> Bool ->
              Core (Int, Term vars)
newMetaLets {vars} fc rig env n ty def nocyc lets
    = do let hty = if lets then abstractFullEnvType fc env ty
                           else abstractEnvType fc env ty
         let hole = record { noCycles = nocyc }
                           (newDef fc n rig [] hty Public def)
         log "unify.meta" 5 $ "Adding new meta " ++ show (n, fc, rig)
         logTerm "unify.meta" 10 ("New meta type " ++ show n) hty
         defs <- get Ctxt
         idx <- addDef n hole
         addHoleName fc n idx
         pure (idx, Meta fc n idx envArgs)
  where
    envArgs : List (Term vars)
    envArgs = let args = reverse (mkConstantAppArgs {done = []} lets fc env []) in
                  rewrite sym (appendNilRightNeutral vars) in args

newMeta : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          {auto u : Ref UST UState} ->
          FC -> RigCount ->
          Env Term vars -> Name -> Term vars -> Def ->
          Bool ->
          Core (Int, Term vars)
newMeta fc r env n ty def cyc = newMetaLets fc r env n ty def cyc False

When a solution is not available, we call newConstant to make a Guess def. A Guess is guarded by some constraints which are generated by unification. The constraints need to be solved before more elaboration can be done. newConstant takes a term which the guess is constructed from and its environment as inputs. It also takes in the list of constraints that need to be satisfied/solved.

mkConstant : {vars : _} ->
             FC -> Env Term vars -> Term vars -> ClosedTerm
mkConstant fc [] tm = tm
mkConstant {vars = x :: _} fc (b :: env) tm
    = let ty = binderType b in
          mkConstant fc env (Bind fc x (Lam fc (multiplicity b) Explicit ty) tm)

-- Given a term and a type, add a new guarded constant to the global context
-- by applying the term to the current environment
-- Return the replacement term (the name applied to the environment)
newConstant : {vars : _} ->
              {auto u : Ref UST UState} ->
              {auto c : Ref Ctxt Defs} ->
              FC -> RigCount -> Env Term vars ->
              (tm : Term vars) -> (ty : Term vars) ->
              (constrs : List Int) ->
              Core (Term vars)
newConstant {vars} fc rig env tm ty constrs
    = do let def = mkConstant fc env tm
         let defty = abstractFullEnvType fc env ty
         cn <- genName "postpone"
         let guess = newDef fc cn rig [] defty Public
                            (Guess def (length env) constrs)
         log "unify.constant" 5 $ "Adding new constant " ++ show (cn, fc, rig)
         logTerm "unify.constant" 10 ("New constant type " ++ show cn) defty
         idx <- addDef cn guess
         addGuessName fc cn idx
         pure (Meta fc cn idx envArgs)
  where
    envArgs : List (Term vars)
    envArgs = let args = reverse (mkConstantAppArgs {done = []} True fc env []) in
                  rewrite sym (appendNilRightNeutral vars) in args

Constraint's (in Core.UnifyState) are pairs of terms (when there is only one constraint) or lists of terms (when there are more than one constraint):

data Constraint : Type where
     -- An unsolved constraint, noting two terms which need to be convertible
     -- in a particular environment
     MkConstraint : {vars : _} ->
                    FC ->
                    (withLazy : Bool) ->
                    (blockedOn : List Name) ->
                    (env : Env Term vars) ->
                    (x : Term vars) -> (y : Term vars) ->
                    Constraint
     -- An unsolved sequence of constraints, arising from arguments in an
     -- application where solving later constraints relies on solving earlier
     -- ones
     MkSeqConstraint : {vars : _} ->
                       FC ->
                       (env : Env Term vars) ->
                       (xs : List (Term vars)) ->
                       (ys : List (Term vars)) ->
                       Constraint
     -- A resolved constraint
     Resolved : Constraint

solveConstraints (in Core.Unify) solves the generated constraints by looking at the UState. It is called not only at the end, but at various times of the elaboration to increase efficiency.

solveConstraints : {auto c : Ref Ctxt Defs} ->
                   {auto u : Ref UST UState} ->
                   UnifyInfo -> (smode : SolveMode) -> Core ()

Meta-variables are not substituted in applications to facilitate sharing.

Unifying constructors (in Core.Unify)

Constructors are injective/cancelable, that is, for example, if Succ x = Succ y then we can conclude x = y. Therefore, we can unify and convert constructors in similar ways: check that the list of arguments correspond. If not, there is no way to unify them and it throws an error.

One needs to be careful about scoping though. Because of dependent types, arguments that are later can depend on earlier arguments, so the order is important.

Unifying blocked applications (in Core.Unify)

unifyApp unifies an application with some values:

unifyApp : {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             {vars : _} ->
             -- swap the order when postponing
             -- (this is to preserve second arg being expected type)
             (swaporder : Bool) -> 
             UnifyInfo -> FC -> Env Term vars -> FC 
             -> NHead vars -- blocked application head
             -> List (Closure vars) -- blocked arguments 
             -> NF vars -- value we're unifying with
             -> Core UnifyResult

For example, unifying plus x Z with Z. The blocked application head is plus, the blocked arguments are x and Z (we cannot solve this at this point, so the application is blocked), and the value we're unifying with is Z.

There are two interesting cases when unifying blocked applications. First, when we're unifying a meta-variable with application. Second, when it's an application that is convertible to the value, then unification is successful even with the blocked application.

Unifying meta-variables (in Core.Unify)

See A tutorial implementation of dynamic pattern unification for more details on pattern unification.

unifyApp swap mode loc env fc (NMeta n i margs) args tm
      = unifyHole swap mode loc env fc n i margs args tm

We need to check that the meta-variable is applied to distinct variables. That is, the arguments margs and args above have to be distinct. If so, we attempt to update the definition of n to n margs args = tm. This will only succeed if variables in tm occur in margs,args.

Unifying other blocked applications that are convertible

-- If they're already convertible without metavariables, we're done,
-- otherwise postpone until later, constraints for now.
  unifyApp False mode loc env fc hd args tm
      = do gam <- get Ctxt
           if !(convert gam env (NApp fc hd args) tm)
              then pure success
              else postponeS True False loc mode "Postponing constraint"
                             env (NApp fc hd args) tm
  unifyApp True mode loc env fc hd args tm
      = do gam <- get Ctxt
           if !(convert gam env tm (NApp fc hd args))
              then pure success
              else postponeS True True loc mode "Postponing constraint"
                             env (NApp fc hd args) tm

Unification in checkExp (in TTImp.Elab.Check)

checkExp checks whether the type we got for the given type matches the expected type. It takes a UState and performs unification when needed and returns the term and its type.

When there are no constraints to be solved, then unification has succeeded and we can try and solve previous unsolved constraints by calling solveConstraints (called by convertWithLazy).

-- Check whether two terms are convertible. May solve metavariables (in Ctxt)
-- in doing so.
-- Returns a list of constraints which need to be solved for the conversion
-- to work; if this is empty, the terms are convertible.
convertWithLazy
        : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          {auto u : Ref UST UState} ->
          {auto e : Ref EST (EState vars)} ->
          (withLazy : Bool) -> (precise : Bool) ->
          FC -> ElabInfo -> Env Term vars -> Glued vars -> Glued vars ->
          Core UnifyResult
convertWithLazy withLazy prec fc elabinfo env x y
    = let umode : UnifyInfo
                = case elabMode elabinfo of
                       InLHS _ => inLHS
                       _ => inTermP prec in
          catch
            (do let lazy = !isLazyActive && withLazy
                logGlueNF 5 ("Unifying " ++ show withLazy ++ " "
                             ++ show (elabMode elabinfo)) env x
                logGlueNF 5 "....with" env y
                vs <- if isFromTerm x && isFromTerm y
                         then do xtm <- getTerm x
                                 ytm <- getTerm y
                                 if lazy
                                    then unifyWithLazy umode fc env xtm ytm
                                    else unify umode fc env xtm ytm
                         else do xnf <- getNF x
                                 ynf <- getNF y
                                 if lazy
                                    then unifyWithLazy umode fc env xnf ynf
                                    else unify umode fc env xnf ynf
                when (holesSolved vs) $
                    solveConstraints umode Normal
                pure vs)
            (\err =>
               do defs <- get Ctxt
                  xtm <- getTerm x
                  ytm <- getTerm y
                  -- See if we can improve the error message by
                  -- resolving any more constraints
                  catch (solveConstraints umode Normal)
                        (\err => pure ())
                  -- We need to normalise the known holes before
                  -- throwing because they may no longer be known
                  -- by the time we look at the error
                  defs <- get Ctxt
                  throw !(normaliseErr (WhenUnifying fc env xtm ytm err)))

export
convert : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          {auto u : Ref UST UState} ->
          {auto e : Ref EST (EState vars)} ->
          FC -> ElabInfo -> Env Term vars -> Glued vars -> Glued vars ->
          Core UnifyResult
convert = convertWithLazy False False

export
convertP : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
           {auto u : Ref UST UState} ->
           {auto e : Ref EST (EState vars)} ->
           (precise : Bool) ->
           FC -> ElabInfo -> Env Term vars -> Glued vars -> Glued vars ->
           Core UnifyResult
convertP = convertWithLazy False

-- Check whether the type we got for the given type matches the expected
-- type.
-- Returns the term and its type.
-- This may generate new constraints; if so, the term returned is a constant
-- guarded by the constraints which need to be solved.
export
checkExpP : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            {auto u : Ref UST UState} ->
            {auto e : Ref EST (EState vars)} ->
            RigCount -> (precise : Bool) -> ElabInfo -> Env Term vars -> FC ->
            (term : Term vars) ->
            (got : Glued vars) -> (expected : Maybe (Glued vars)) ->
            Core (Term vars, Glued vars)
checkExpP rig prec elabinfo env fc tm got (Just exp)
    = do vs <- convertWithLazy True prec fc elabinfo env got exp
         case (constraints vs) of
              [] => case addLazy vs of
                         NoLazy => do logTerm 5 "Solved" tm
                                      pure (tm, got)
                         AddForce r => do logTerm 5 "Force" tm
                                          logGlue 5 "Got" env got
                                          logGlue 5 "Exp" env exp
                                          pure (TForce fc r tm, exp)
                         AddDelay r => do ty <- getTerm got
                                          logTerm 5 "Delay" tm
                                          pure (TDelay fc r ty tm, exp)
              cs => do logTerm 5 "Not solved" tm
                       defs <- get Ctxt
                       empty <- clearDefs defs
                       cty <- getTerm exp
                       -- we haven't solved it so we're making a guess
                       ctm <- newConstant fc rig env tm cty cs
                       -- tm is the guess for the solution under constraints cs
                       dumpConstraints 5 False
                       case addLazy vs of
                            NoLazy => pure (ctm, got)
                            AddForce r => pure (TForce fc r tm, exp)
                            AddDelay r => do ty <- getTerm got
                                             pure (TDelay fc r ty tm, exp)
checkExpP rig prec elabinfo env fc tm got Nothing = pure (tm, got)

export
checkExp : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
           {auto u : Ref UST UState} ->
           {auto e : Ref EST (EState vars)} ->
           RigCount -> ElabInfo -> Env Term vars -> FC ->
           (term : Term vars) ->
           (got : Glued vars) -> (expected : Maybe (Glued vars)) ->
           Core (Term vars, Glued vars)
checkExp rig elabinfo = checkExpP rig (preciseInf elabinfo) elabinfo

Elaborating Implicits with checkTerm (in TTImp.Elab.Term)

Where do meta-variables come from? Why do we need unification to solve them? The answer is Implicit, as in TTImp.TTImp:

data RawImp : Type where
       ...
       -- An implicit value, solved by unification, but which will also be
       -- bound (either as a pattern variable or a type variable) if unsolved
       -- at the end of elaborator
       Implicit : FC -> (bindIfUnsolved : Bool) -> RawImp

       -- with-disambiguation
       IWithUnambigNames : FC -> List Name -> RawImp -> RawImp

During type checking, when we encounter an Implicit, we make a meta-variable with the expected type, and hope that unifying the meta-variable and the expected type will succeed.

checkTerm rig elabinfo nest env (Implicit fc b) (Just gexpty)
    = do nm <- genName "_" -- create a new name for the expected type
         expty <- getTerm gexpty -- get the expected type
         -- generate a meta-variable for the implicit, with the expected type
         metaval <- metaVar fc rig env nm expty
         -- Add to 'bindIfUnsolved' if 'b' set
         ...
         pure (metaval, gexpty)

Similarly for implicit arguments in types. For example,

reverse : {a: Type} -> List a -> List a

{a: Type} is the implicit argument. When checking applications, we first look at the function's type. If there's an implicit argument, create a meta-variable for it (like above) and continue checking the application.

Idris 2 has explicit pattern variable binding. When checkTerm encounters an IBindVar, it notes the name (of type String, the second input) and the expected type. It creates a pattern meta-variable for the pattern.

data RawImp : Type where
       ...
-- A name which should be implicitly bound
       IBindVar : FC -> String -> RawImp

At the end of elaboration, we pattern bind all the names we noted (and any names which depend on it). This involves sorting variables into dependency order. The swap function in Idris 2 optimizes the naming and keeps track of the order etc.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment