TypeFamilies vs. etc - restrined instance overlap type inference

[Anthony Clayden]

Hi all some more,

Continuing the idea of a restrained form of instance overlap
for type functions ...

Type inference I don't expect to be totally decidable, so
that may torpedo the idea altogether. I do expect it to be
more coherent than GHC's current handling of overlap with
fundeps. What's impressive is how much of a 'cottage
industry' has grown up using overlaps. Do we really want to
throw all that away?

SPJ summarises that the idea is that:
> ... type inference only picks
> an equation when all the earlier equations are guaranteed
> not to match.  So there is no danger of making different
> choices in different parts of the program (which is what
> gives rise to unsoundness).

In my earlier post I proposed how to validate instances so
that they don't overlap (although the instance heads might
do), by using type inequality restraints.

In an ancient mail list discussion of similar ideas
[haskell-prime February 2006 'overlapping instances and
constraints'] when type families were first mooted,
 SPJ commented:
	"Concerning [a suggested approach] it involves *search*
which the
	current mechanism does not.  Presumably you have in mind
that the 
	type system should "commit" only when there is only one
remaining 
	instance declaration that can fit.  You need to be very
careful not 
	to prune off search branches prematurely, because in a
traditional 
	HM type checker you don't know what all the type are
completely.  
	And you need to take functional dependencies into account
during the 
	search (but not irrevocably).   I have not implemented this
in GHC.  
	I don't know anyone who has.   I don't even know anyone who
has
	specified it.


	All good stuff to debate.  [...] In general, I think that
	type-system proposals are much easier to evaluate when
accompanied with
	formal type rules.  It's not just a macho thing -- it
really helps in
	debugging the dark corners. "

Inference for instances without restraints proceeds as
usual.

Instances with type inequality restraints are validated not
to overlap those without, so if there's an instance that
fits, we can apply it confidently.

What we do need is rules for how type inference gathers
evidence of a type inequality from the type environment.
Once we've inferred that evidence, we can 'fit' to the
instance head and apply the RHS of the type function (or
apply the type Class).

Evidence of type inequality:
Base case:    T t1 t2 ... tn /~ U u1 u2 ... um, where T, U
type constructors and T /= U
                                                 n, m >= 0
Derived case: T t1 t2 ... tn /~ T u1 u2 ... un, where T type
constructor
                     And ti /~ ui for some i
           (I suspect this is far as GHC tries currently to
discriminate overlaps,
            based on the groundedness experiments discussed
in the HList paper section 9.
            I think it's possible to get a bit further ...)

also derived: t t1 t2 ... tn /~ t u1 u2 ... un, where t is a
type term AND ti /~ ui
              (t can be type term except a type function)
and:          T t1 t2 ... tn /~ t u1 u2 ... un, if ti /~ ui,
where T type constructor
              (again t can be any type term except a type
function
               note that matching type args is from the
right-hand end,
               because t might turn out to be of the form
(tt uu1 uu2 ...)
               essentially: whatever t resolves to, the
overall types must be unequal)
as well:      T t1 t2 ... tn /~ t u1 u2 ... um, where T type
constructor And m > n
              (t any type term except a type function,
               if m > n then t's arity is more than T's, so
they can't be the same.)


Algebra:
     Type inequality is symmetric: t /~ u ==> u /~ t
       transitive across equality: t /~ u, u ~ v ==> t /~ v


My (highly hand-wavy) understanding from the 'outside-in'
papers of how type inference proceeds is that the possible
instances 'compete' to apply until one fits. (If there would
be several that might fit, it's 'first come first served'.
So it's essential under GHC's current forms of type families
that overlapping instances are confluent.) With type
inequality restraints we keep to that rule: inference must
not apply an instance until the type environment provides
evidence of the inequality.


AntC