-(gadtRefine cvs) takes a list of coercion variables, and returns a
-list of coercions, obtained by unifying the types equated by the
-incoming coercions. The returned coercions all have kinds of form
-(a:=:ty), where a is a rigid type variable.
-
-Example:
- gadtRefine [c :: (a,Int):=:(Bool,b)]
- = [ right (left c) :: a:=:Bool,
- sym (right c) :: b:=:Int ]
-
-That is, given evidence 'c' that (a,Int)=(Bool,b), it returns derived
-evidence in easy-to-use form. In particular, given any e::ty, we know
-that:
- e `cast` ty[right (left c)/a, sym (right c)/b]
- :: ty [Bool/a, Int/b]
-
-Two refinements:
-
-- It can fail, if the coercion is unsatisfiable.
-
-- It's biased, by being given a set of type variables to bind
- when there is a choice. Example:
- MkT :: forall a. a -> T [a]
- f :: forall b. T [b] -> b
- f x = let v = case x of { MkT y -> y }
- in ...
- Here we want to bind [a->b], not the other way round, because
- in this example the return type is wobbly, and we want the
- program to typecheck
-
-
--- E.g. (a, Bool, right (left c))
--- INVARIANT: in the triple (tv, ty, co), we have (co :: tv:=:ty)
--- The result is idempotent: the
+Given a list of coercions, where for each coercion c::(ty1~ty2), the type ty2
+is a specialisation of ty1, produce a type refinement that maps the variables
+of ty1 to the corresponding sub-terms of ty2 using appropriate coercions; eg,
+
+ matchRefine (co :: [(a, b)] ~ [(c, Maybe d)])
+ = { right (left (right co)) :: a ~ c
+ , right (right co) :: b ~ Maybe d
+ }
+
+Precondition: The rhs types must indeed be a specialisation of the lhs types;
+ i.e., some free variables of the lhs are replaced with either distinct free
+ variables or proper type terms to obtain the rhs. (We don't perform full
+ unification or type matching here!)
+
+NB: matchRefine does *not* expand the type synonyms.