Version 95 (modified by chak, 8 years ago) (diff) 

Entailment of Type Equalities
Our aim is to derive the entailment judgement
g1, .., gn  w1, .., wm
i.e., whether we can derive the wanted equalities w1 to wm from the given equalities g1, .., gn under a given set of toplevel equality schemas (i.e., equalities involving universally quantified variables). We permit unification variables in the wanted equalities, and a derivation may include the instantiation of these variables; i.e., may compute a unifier. However, that unifer must be most general.
The derivation algorithm is complicated by the pragmatic requirement that, even if there is no derivation for the judgement, we would like to compute a unifier. This unifier should be as specific as possible under some not yet specified (strongest) weakening of the judgement so that it is derivable. (Whatever that means...)
The following is based on ideas for the new, postICFP'08 solving algorithm described in CVS papers/typesynonym/newsingle.tex. A revised version of newsingle.tex that integrates the core ideas from this wiki page is in papers/typesynonym/normalised_equations_algorithm.tex. Most of the code is in the module TcTyFuns.
Terminology
 Wanted equality
 An equality constraint that we need to derive during type checking. Failure to derive it leads to rejection of the checked program.
 Local equality, given equality
 An equality constraint that in a certain scope may be used to derive wanted equalities.
 Flexible type variable, unification variable, HM variable
 Type variables that may be globally instantiated by unification. We use Greek letters alpha, beta,... as names for these variables.
 Rigid type variable, skolem type variable
 Type variable that cannot be globally instantiated, but it may be locally refined by a local equality constraint. We use Roman letters a, b,... as names for these variables.
In positions where we can have both flexible and rigid variables, we use x, y, z.
Overall algorithm
The overall structure is as in newsingle.tex, namely
 normalise all constraints (both locals and wanteds),
 solve the wanteds, and
 finalise.
However, the three phases differ in important ways. In particular, normalisation includes decompositions & the occurs check, and we don't instantiate any flexible type variables before we finalise (i.e., solving is purely local).
Normal equalities
Central to the algorithm are normal equalities, which can be regarded as a set of rewrite rules. Normal equalities are carefully oriented and contain synonym families only as the head symbols of lefthand sides. They assume one of the following two major forms:
 Family equality: co :: F t1..tn ~ t or
 Variable equality: co :: x ~ t, where we again distinguish two forms:
 Variableterm equality: co :: x ~ t, where t is not a variable, or
 Variablevariable equality: co :: x ~ y, where x > y.
where
 the types t, t1, ..., tn may not contain any occurrences of synonym families,
 the lefthand side of an equality may not occur in the righthand side, and
 the relation x > y is an arbitrary, but total order on type variables.
The second bullet of the where clause is trivially true for equalities of Form (1); it also implies that the left and righthand sides are different.
Furthermore, we call a variable equality whose lefthand side is a flexible type variable (aka unification variable) a flexible variable equality, and correspondingly, a variable equality whose lefthand side is a rigid type variable (aka skolem variable) a rigid variable equality.
Observations
The following is interesting to note:
 Normal equalities are similar to equalities meeting the Orientation Invariant and Flattening Invariant of newsingle, but they are not the same.
 Normal equalities are never selfrecursive. They can be mutually recursive. A mutually recursive group will exclusively contain variable equalities.
Coercions
Coercions co are either wanteds (represented by a flexible type variable) or givens aka locals (represented by a type term of kind CO). In GHC, they are represented by TcRnTypes.EqInstCo, which is defined as
type EqInstCo = Either TcTyVar  case for wanteds (variable to be filled with a witness) Coercion  case for locals
Moreover, TcTyFuns.RewriteInst represents normal equalities, emphasising their role as rewrite rules.
SLPJ: I propose that we use a proper data type, not Either for this.
Normalisation
The following function norm turns an arbitrary equality into a set of normal equalities.
data EqInst  arbitrary equalities data FlatEqInst  synonym families may only occur outermost on the lhs data RewriteInst  normal equality norm :: EqInst > [RewriteInst] norm [[co :: F s1..sn ~ t]] = [[co' :: F s1'..sn' ~ t']] : eqs where (s1', c1, eqs1) = flatten s1 .. (sn', cn, eqsn) = flatten sn (t', c, eqt) = flatten t (co', eqs) = adjust co (F c1..cn) (sym c) (eqs1++..++eqsn++eqt) norm [[co :: t ~ F s1..sn]] = norm [[co' :: F s1..sn ~ t]] with co = sym co' norm [[co :: s ~ t]] = check [[co' :: s' ~ t']] ++ eqs where (s', cs, eqs) = flatten s (t', ct, eqt) = flatten t (co', eqs) = adjust co cs (sym ct) (eqs ++ eqt) check :: FlatEqInst > [RewriteInst]  Does OccursCheck + Decomp + Triv + Swap (of newsingle) check [[co :: t ~ t]] = [] with co = id check [[co :: x ~ y]]  x > y = [[co :: x ~ y]]  otherwise = [[co' :: y ~ x]] with co = sym co' check [[co :: x ~ t]]  x `occursIn` t = fail  otherwise = [[co :: x ~ t]] check [[co :: t ~ x]]  x `occursIn` t = fail  otherwise = [[co' :: x ~ t]] with co = sym co' check [[co :: s1 s2 ~ t1 t2]] = check [[col :: s1 ~ t1]] ++ check [[cor :: s2 ~ t2]] with co = col cor check [[co :: T ~ S]] = fail flatten :: Type > (Type, Coercion, [RewriteInst])  Result type has no synonym families whatsoever flatten [[F t1..tn]] = (alpha, [[F c1..cn > gamma]], [[gamma :: F t1'..tn' ~ alpha]] : eqt1++..++eqtn) where (t1', c1, eqt1) = flatten t1 .. (tn', cn, eqtn) = flatten tn FRESH alpha, gamma RECORD alpha := F t1..tn IF local equality flatten [[t1 t2]] = ([[t1' t2']], [[c1 c2]], eqs++eqt) where (t1', c1, eqs) = flatten t1 (t2', c2, eqt) = flatten t2 flatten t = (t, t, []) adjust :: EqInstCo > Coercion > Coercion > [RewriteInst] > (EqInstCo, [RewriteInst])  Adjust coercions depending on whether we process a local or wanted equality adjust co co1 co2 eqs@[[co1 :: s1 ~ t1, .., con :: sn ~ tn]]  isWanted co = (co_new, eqs) with co = co1 > co_new > co2  otherwise = (co, [[id :: s1 ~ t1, .., id :: sn ~ tn]])
Notes:
 Perform Rule Triv & Decomp as part of normalisation.
 Whenever an equality of Form (2) or (3) would be recursive, the program can be rejected on the basis of a failed occurs check. (Immediate rejection is always justified, as righthand sides do not contain synonym familles; hence, any recursive occurrences of a lefthand side imply that the equality is unsatisfiable.)
 For all local equalities, we RECORD substitutions for fresh flexibles introduced by flatten by already updating the meta type variable. However, the update will only have an effect after the Insts have been zonked; i.e., after finalisation.
 We drop all loopy equalities (see Section 8.2 of our ICFP'08 paper). If we drop a wanted, it is a type error; if we drop a local, we emit a warning (as we only sacrifice completeness).
 We do the essentially same for class constraints; i.e., we use flatten to extract all family applications as equality constraints. However, instead of adjusting the coercion at the flattened constraint, we generate a dictionary binding for the new dictionary (using a cast expression).
Propagation (aka Solving)
Propagation is based on four rules that transform family and variable equalities. The first rule transforms a family equality using a toplevel equality schema. The other three use one equality to transform another. In the presentation, the transforming equality is always first and the transformed is second, separate by an ampersand (&).
Below the rules are two scheme for applying the rules. The first one naively iterates until the system doesn't change anymore. The second scheme optimises the iteration somewhat.
Rules
 Top

co :: F t1..tn ~ t =(Top)=> co' :: [s1/x1, .., sm/xm]s ~ t with co = g s1..sm > co'
where g :: forall x1..xm. F u1..um ~ s and [s1/x1, .., sm/xm]u1 == t1.
NB: Afterwards, we need to normalise. Then, any of the four propagation rules may apply.
 SubstFam

co1 :: F t1..tn ~ t & co2 :: F t1..tn ~ s =(SubstFam)=> co1 :: F t1..tn ~ t & co2' :: t ~ s with co2 = co1 > co2'
where co1 may be a wanted only if co2 is a wanted, too.
NB: Afterwards, we need to normalise co2'. Then, the SubstVarVar or SubstVarFam rules may apply to the results of normalisation. Moreover, co1 may have a SubstFam or a SubstVarFam match with rules other than the results of normalising co2'.
 SubstVarVar

co1 :: x ~ t & co2 :: x ~ s =(SubstVarVar)=> co1 :: x ~ t & co2' :: t ~ s with co2 = co1 > co2'
where co1 may be a wanted only if co2 is a wanted, too.
NB: Afterwards, we need to normalise co2'. Then, the SubstVarVar or SubstVarFam rules may apply to the results of normalisation, but not with co1, as s and t cannot contain x  cf. the definition of normal equalities. However, co1 may have another SubstVarVar or SubstVarFam match with rules other than the results of normalising co2'.
 SubstVarFam

co1 :: x ~ t & co2 :: F s1..sn ~ s =(SubstVarFam)=> co1 :: x ~ t & co2' :: [t/x](F s1..sn) ~ s with co2 = [co1/x](F s1..sn) > co2'
where x occurs in F s1..sn, and co1 may be a wanted only if co2 is a wanted, too.
NB: No normalisation required. Afterwards, SubstVarVar or SubstVarFam may apply to co1 and all rules, except SubstVarVar, may apply to co2'. However, SubstVarFam cannot again apply to co1 and co2', as t cannot contain x  cf. the definition of normal equalities.
NB: In the three substitution rules, it is never necessary to try using co1 with any of the equalities derived from co2'. Hence, after having considered one equality as co1 with every other equality, we can immediately put co1 into the list of residual equalities.
Rule application: specification
Propagation proceeds by applying any of the four rules until the system does not change anymore. After application of a rule, the equalities that were modified need to be normalised again:
Propagate = fix (Top  SubstFam  SubstVarVar  SubstVarFam)
Rule application: algorithm
The following function gets a list with all local and wanted equalities. It returns a list of residual equalities that permit no further rule application.
 all four rule functions return Nothing if rule not applicable applyTop :: RewriteInst > Maybe EqInst applySubstFam :: RewriteInst > RewriteInst > Maybe EqInst  return only... applySubstVarVar :: RewriteInst > RewriteInst > Maybe EqInst  ...the modified... applySubstVarFam :: RewriteInst > RewriteInst > Maybe EqInst  ...equality propagate :: [RewriteInst] > [RewriteInst] propagate eqs = prop eqs [] where prop :: [RewriteInst]  todo list (still need to try these equalities) > [RewriteInst]  residual list (tried all equalities here already pairwise) > [RewriteInst]  these permit no further rule application prop [] res = res prop (eq:eqs) res = apply eq eqs res apply eq eqs res  Just eq' < applyTop eq = prop (norm eq' ++ eqs) res  otherwise = let (new_eqs, unchanged_eqs) = mapAndUnzip (applySubstRules eq) eqs (new_res, unchanged_res) = mapAndUnzip (applySubstRules eq) res in prop (concat new_eqs ++ concat new_res ++ concat unchanged_eqs) (eq : concat unchanged_res) applySubstRules eq1 eq2  Just eq2' < applySubstFam eq1 eq2 = (norm eq2', [])  Just eq2' < applySubstVarVar e1 eq2 = (norm eq2', [])  Just eq2' < applySubstVarFam eq1 eq2 = ([eq2'], [])  otherwise = ([], [eq2])
Observations
 Only SubstVarFam when replacing a variable in a family equality can lead to recursion with (Top).
 A significant difference to newsingle is that solving is a purely local operation. We never instantiate any flexible variables.
 We cannot discard any variable equalities after substitution since we do not substitute into righthand sides anymore. Moreover, in the concrete implementation, variables may also be reintroduced due to simplification of type classes (which currently doesn't happen in the same iteration).
Finalisation
The finalisation step instantiates as many flexible type variables as possible, but it takes care not to instantiate variables occurring in the global environment with types containing synonym family applications. This is important to obtain principle types (c.f., Andrew Kennedy's thesis). We perform finalisation in two phases:
 Substitution: For any variable equality of the form co :: x ~ t (both local and wanted), we apply the substitution [t/x] to the lefthand side of all equalities. We also perform the same substitution on all class constraints.
 Instantiation: For any variable equality of the form co :: alpha ~ t or co :: a ~ alpha, where co is wanted, we instantiate alpha with t or a, respectively, and set co := id. Moreover, we have to do the same for equalities of the form co :: F t1..tn ~ alpha unless we are in inference mode and alpha appears in the environment or any other wanteds. (We never instantiate any flexibles introduced by flattening locals.)
The substitution step can lead to recursive equalities; i.e., we need to apply an occurs check after each substitution. It is an important property of propagation that we only need to substitute into righthand sides during finalisation.
After finalisation and zonking all flattening of locals is undone (c.f., note below the flattening code above).
Examples
Unflattening locals and finalisation
This seems ok:
c :: a ~ [F b]  gamma :: alpha ~ a =(norm)=> c :: a ~ [beta], id :: F b ~ beta  gamma :: alpha ~ a with beta := F b =(final)=> alpha := a, gamma := id
The problem becomes obvious when we orient the wanted equality the other way around:
c :: a ~ [F b]  gamma :: a ~ alpha =(norm)=> c :: a ~ [beta], id :: F b ~ beta  gamma :: a ~ alpha =(SubstVarVar)=> c :: a ~ [beta], id :: F b ~ beta  gamma' :: [beta] ~ alpha with gamma := c > gamma' =(norm)=> c :: a ~ [beta], id :: F b ~ beta  gamma'' :: alpha ~ [beta] with gamma' := sym gamma'' =(final)=> alpha := [F b], gamma'' := id
This result is fine, even when considering Andrew Kennedy's concerns, as we are necessarily in checking mode (following the normalised_equation_algorithm terminology).
Let's assume one toplevel equality forall x. g x :: F x = ():
c :: a ~ [F b]  gamma :: a ~ alpha =(norm)=> c :: a ~ [beta], id :: F b ~ beta  gamma :: a ~ alpha with beta := F b =(SubstVarVar)=> c :: a ~ [beta], id :: F b ~ beta  gamma' :: [beta] ~ alpha with gamma := c > gamma' =(norm)=> c :: a ~ [beta], id :: F b ~ beta  gamma'' :: alpha ~ [beta] with gamma' := sym gamma'' =(Top)=> c :: a ~ [beta], sym (g b) :: () ~ beta  gamma'' :: alpha ~ [beta] =(norm)=> c :: a ~ [beta], g b :: beta ~ ()  gamma'' :: alpha ~ [beta] =(final)=> alpha := [()], gamma'' := id
NB: The algorithm in the normalisied_equalities_algorithm paper (as opposed to the on this wiki page) will compute alpha := [F b], which is equivalent, but less normalised.
TODO Still need to adapt the following examples to new rule set!
Substituting wanted family equalities with SubstFam is crucial if the righthand side contains a flexible type variable
Top: F Int ~ [Int]  F delta ~ [delta], F delta ~ [Int] (SubstFam)  F delta ~ [delta], norm [[ [delta] ~ [Int] ]] ==>  F delta ~ [delta], delta ~ Int (SubstVar)  norm [[ F Int ~ [Int] ]], delta ~ Int ==>  F Int ~ [Int], delta ~ Int (Top)  norm [[ [Int] ~ [Int] ]], delta ~ Int ==>  delta ~ Int QED
Interaction between local and wanted family equalities
Example 4 of Page 9 of the ICFP'09 paper.
F [Int] ~ F (G Int)  G Int ~ [Int], H (F [Int]) ~ Bool =(norm)=> F [Int] ~ a, F b ~ a, G Int ~ b  G Int ~ [Int], H x ~ Bool, F [Int] ~ x (SubstFam w/ F [Int]) F [Int] ~ a, F b ~ a, G Int ~ b  G Int ~ [Int], H x ~ Bool, x ~ a (SubstFam w/ G Int) F [Int] ~ a, F b ~ a, G Int ~ b  b ~ [Int], H x ~ Bool, x ~ a (SubstVar w/ x) F [Int] ~ a, F b ~ a, G Int ~ b  b ~ [Int], H a ~ Bool, x ~ a
TODO If we use flexible variables for the flattening of the wanteds, too, the equality corresponding to x ~ a above will be oriented the other way around. That can be a problem because of the asymmetry of the SubstVar and SubstFun rules (i.e., wanted equalities are not substituted into locals).
Termination
SkolemOccurs
The Note [skolemOccurs loop] in the old code explains that equalities of the form x ~ t (where x is a flexible type variable) may not be used as rewrite rules, but only be solved by applying Rule Unify. As Unify carefully avoids cycles, this prevents the use of equalities introduced by the Rule SkolemOccurs as rewrite rules. For this to work, SkolemOccurs also had to apply to equalities of the form a ~ t[[a]]. This was a somewhat intricate set up that we seek to simplify here. Whether equalities of the form x ~ t are used as rewrite rules or solved by Unify doesn't matter anymore. Instead, we disallow recursive equalities after normalisation completely (both locals and wanteds). This is possible as righthand sides are free of synonym families.
To look at this in more detail, let's consider the following notorious example:
E_t: forall x. F [x] ~ [F x] [F v] ~ v  [F v] ~ v
Newsingle: The following derivation shows how the algorithm in newsingle fails to terminate for this example.
[F v] ~ v  [F v] ~ v ==> normalise v ~ [a], F v ~ a  v ~ [x], F v ~ x a := F v ==> (Local) with v F [a] ~ a  [a] ~ [x], F [a] ~ x ==> normalise F [a] ~ a  x ~ a, F[a] ~ x ==> 2x (Top) & Unify [F a] ~ a  [F a] ~ a ..and so on..
Newsingle using flexible tyvars to flatten locals, but w/o Rule (Local) for flexible type variables: With (SkolemOccurs) it is crucial to avoid using Rule (Local) with flexible type variables. We can achieve a similar effect with newsingle if we (a) use flexible type variables to flatten local equalities and (b) at the same time do not use Rule (Local) for variable equalities with flexible type variables. NB: Point (b) was necessary for the ICFP'08 algorithm, too.
[F v] ~ v  [F v] ~ v ==> normalise v ~ [x2], F v ~ x2  v ~ [x1], F v ~ x1 ** x2 := F v ==> (Local) with v F [x2] ~ x2  [x2] ~ [x1], F [x2] ~ x1 ** x2 := F v ==> normalise F [x2] ~ x2  x2 ~ x1, F [x2] ~ x1 ** x2 := F v ==> 2x (Top) & Unify [F x1] ~ x1  [F x1] ~ x1 ** x1 := F v ==> normalise x1 ~ [y2], F x1 ~ y2  x1 ~ [y1], F x1 ~ y1 ** x1 := F v, y2 := F x1 ..we stop here if (Local) doesn't apply to flexible tyvars
A serious disadvantage of this approach is that we do want to use Rule (Local) with flexible type variables as soon as we have rankn signatures. In fact, the lack of doing so is responsible for a few failing tests in the testsuite in the GHC implementation of (SkolemOccurs).
Deprioritise Rule (Local): Instead of outright forbidding the use of Rule (Local) with flexible type variables, we can simply require that Local is only used if no other rule is applicable. (That has the same effect on satisfiable queries, and in particular, the present example.)
[F v] ~ v  [F v] ~ v ==> normalise v ~ [a], F v ~ a  v ~ [x], F v ~ x a := F v ==> (IdenticalLHS) with v & F v v ~ [a], F v ~ a  [a] ~ [x], x ~ a ==> normalise v ~ [a], F v ~ a  x ~ a, x ~ a ==> (Unify) v ~ [a], F v ~ a  a ~ a ==> normalise v ~ [a], F v ~ a  QED
In fact, it is sufficient to deprioritise Rule (Local) for variable equalities (if it is used for other equalities at all):
[F v] ~ v  [F v] ~ v ==> normalise v ~ [a], F v ~ a  v ~ [x], F v ~ x a := F v ==> (Local) with F v v ~ [a], F v ~ a  v ~ [x], x ~ a ==> (Unify) v ~ [a], F v ~ a  v ~ [a] ==> (Local) with v v ~ [a], F [a] ~ a  [a] ~ [a] ==> normalise v ~ [a], F [a] ~ a  QED
One problems remains: The algorithm still fails to terminate for unsatisfiable queries.
[F v] ~ v  [G v] ~ v ==> normalise v ~ [a], F v ~ a  v ~ [x], G v ~ x a := F v ==> (Local) with v F [a] ~ a  [a] ~ [x], G [a] ~ x ==> normalise F [a] ~ a  x ~ a, G [a] ~ x ==> (Unify) F [a] ~ a  G [a] ~ a ==> (Top) [F a] ~ a  G [a] ~ a ==> normalise a ~ [b], F a ~ b  G [a] ~ a b := F a ..and so on..
My guess is that the algorithm terminates for all satisfiable queries. If that is correct, the entailment problem that the algorithm solves would be semidecidable.
Derivation with latest (and implemented) algorithm:
Top: forall x. F x ~ [F x] F [a] ~ a  =(norm)=> F [a] ~ a  =(Top)=> [F a] ~ a  =(norm)=> a ~ [beta], F a ~ beta  with beta := F a =(SubtVarFam)=> a ~ [beta], F [beta] ~ beta  ...and so on...
The only solution seems to be to give up on completeness and throw away loopy equalities as proposed in the ICFP'08 paper.