Equality constraints (~): type-theory behind them

[Adam Gundry]

Hi AntC [with apologies for the duplicate email],

Regarding inference, the place that comes to mind is Vytiniotis et al.
OutsideIn(X): Modular type inference with local assumptions. JFP 2011.
<https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/jfp-outsidein.pdf>.

On the underlying core language, there are various papers starting with
Sulzmann et al. System F with type equality coercions. TLDI 2007.
<https://www.microsoft.com/en-us/research/wp-content/uploads/2007/01/tldi22-sulzmann-with-appendix.pdf>

About your specific question, if a wanted constraint `a ~ b` can be
solved by unifying `a` with `b`, then GHC is free to do so (in a sense,
either parameter of (~) can be improved from the other). The real
difference with `TypeCast` arises when local equality assumptions (given
constraints) are involved, because then there may be wanted constraints
that cannot be solved by unification but can be solved by exploiting the
local assumptions.

For example, consider this function:

    foo :: forall a b . a ~ b => [a] -> [b]
    foo x = x

When checking the RHS of `foo`, a wanted constraint `[a] ~ [b]` arises
(because `x` has type `[a]` and is used in a place where `[b]` is
expected). Since `a` and `b` are universally quantified variables, this
cannot be solved by unification. However, the local assumption (given
constraint) `a ~ b` can be used to solve this wanted.

This is rather like automatically inferring where `typeCast` needs to be
placed (indeed, at the Core level there is a construct for casting by an
equality proof, which plays much the same role).

Hope this helps,

Adam


On 06/12/2018 12:01, Anthony Clayden wrote:
> The (~) constraint syntax is enabled by either `GADTs` or `TypeFamilies`
> language extension.
> 
> GADTs/Assoc Data Types/Assoc Type Synonyms/Type Families arrived in a
> series of papers 2005 to 2008, and IIRC the development wasn't finished
> in full in GHC until after that. (Superclass constraints took up to
> about 2010.)
> 
> Suppose I wanted just the (~) parts of those implementations. Which
> would be the best place to look? (The Users Guide doesn't give a
> reference.) ICFP 2008 'Type Checking with Open Type Functions' shows
> uses of (~) in user-written code, but doesn't explain it or motivate it
> as a separate feature.
> 
> My specific question is: long before (~), it was possible to write a
> TypeCast class, with bidirectional FunDeps to improve each type
> parameter from the other. But for the compiler to see the type
> improvement at term level, typically you also need a typeCast method and
> to explicitly wrap a term in it. If you just wrote a term of type `a` in
> a place where `b` was wanted, the compiler would either fail to see your
> `TypeCast a b`, or unify the two too eagerly, then infer an overall type
> that wasn't general enough.
> 
> (For that reason, the instance for TypeCast goes through some
> devious/indirect other classes/instances or exploits separate
> compilation, to hide what's going on from the compiler's enthusiasm.)
> 
> But (~) does some sort of magic: it's a kinda typeclass but without a
> method. How does it mesh with type improvement in the goldilocks zone:
> neither too eager nor too lazy?
> 
> 
> AntC


-- 
Adam Gundry, Haskell Consultant
Well-Typed LLP, https://www.well-typed.com/