Skip to content

Clarify error messages when there is a kind mismatch

Create a module with the following code:

{-# LANGUAGE PolyKinds, TypeFamilies #-}
module T9171 where
data Base

type family GetParam (p::k1) (t::k2) :: k3

type instance GetParam Base t = t

It loads into GHCi just fine. But when we run:

ghci> :t undefined :: GetParam Base (GetParam Base Int)

we get an error

<interactive>:1:14:
    Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
                with actual type ‘GetParam Base (GetParam Base Int)’
    NB: ‘GetParam’ is a type function, and may not be injective
    The type variable ‘k0’ is ambiguous
    In the ambiguity check for: GetParam Base (GetParam Base Int)
    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
    In an expression type signature: GetParam Base (GetParam Base Int)
    In the expression: undefined :: GetParam Base (GetParam Base Int)

If we modify the module by either

  1. set k3 to k2, k1, or any concrete kind

or

  1. set k2 to any concrete kind

then the ghci snippet will type check just fine.

I assume that this is a mistake, and that the original code should work just fine. If there is some reason, however, why the program would be unsound, then the error message should be made a bit more informative. The claim is that the kind k0 is ambiguous, but it doesn't appear anywhere in my code! In my full program, it took me a long time to narrow down that this was the source of the problem.

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