Impact of type families on type inference

Learn
1

I’m reading Higher-order Type-level Programming in Haskell, and I have some questions. This is one.

Here’s a paragraph from page 3, §2.3:

2.3.1 Inference. Consider the call (f x), where f :: Monad m => m a -> m a, and x :: F Int for some type family F. Is the call well-typed? We must instatiate f with suitable types tm and ta, and then we need to satisfy the “wanted” equality (see Section 5.1) tm ta ~ F Int, where (~) means type equality. How can we do that? You might think that tm = F and ta = Int would work, and so it might. But suppose F Int reduces to Maybe Bool; then tm=Maybe and ta=Bool would also work. Worse, if F Int reduces to Bool then the program is ill-typed.

My first reaction upon reading it was along the lines of “so what?”, in the sense that it felt all clear. Also, regarding the part

Worse, if F Int reduces to Bool then the program is ill-typed.

I even thuoght “lucky us, as we do want the program to fail type-checking, in this case”, don’t we?

So I went on to the following paragraph:

So, during type inference, GHC never decomposes “wanted” equalities headed by a type family, like tm ta ~ F Int. But given a wanted equality like tm ta ~ Maybe Int GHC does (and must) decompose it into two simpler wanted equalities tm ~ Maybe and ta ~ Int.

I know it all sounds simple, but I feel the need to reword the above in a way that better resonates with me and somebody tell me if I’m correct.

Do I understand that the bottom line is that type families are “eagerly applied” before the type checking phase?

As in, with reference to the examples in the first excerpt, given tm ta ~ F Int, the type checker would first of all “eagerly” apply the type family, so that F is eliminated, and then proceed to either assign tm = Maybe and ta = Bool (in case F Int reduces to Maybe Bool) or reject the code as ill-typed (if F Int reduces to Bool)?

1 Like
2

Mmm. As eagerly as possible, but no eagerlier. And certainly not before type checking.

Because Type Families are defined via instances, and those might be Overlapping– in the case of Closed TFs.

And typechecking might not be able to narrow down which instance to pick until it has improved the type argument enough at the TF’s call site.

So TF instantiation has to be intermingled with type improvement in general.