Notify user when a kind mismatch holds up a type family reduction
Consider this contrived example:
{-# LANGUAGE TypeFamilies, PolyKinds, UndecidableInstances #-}
module Bug where
import Data.Proxy
type family F (a :: k) :: k
type instance F a = G a
type family G a
type instance G a = a
foo :: Proxy (F Maybe) -> Proxy Maybe
foo = id
This (correctly) fails to compile. The error message is
Bug.hs:14:7:
Couldn't match type ‘F Maybe’ with ‘Maybe’
Expected type: Proxy (F Maybe) -> Proxy Maybe
Actual type: Proxy Maybe -> Proxy Maybe
In the expression: id
In an equation for ‘foo’: foo = id
Failed, modules loaded: none.
But this is peculiar, but it surely looks like F
should be a type-level identity function! Of course, upon further inspection, we see that F
is partial. It reduces only at kind *
. This is quite hard to figure out, though, especially given that we're using the "default to *
" behavior of open type families to arrange for this kind restriction.
Thus, I propose: figure out when a type family reduction is held up due to a kind mismatch, and inform the user.