Skip to content

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.

Edited by Ben Gamari
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information