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
- set
k3
tok2
,k1
, or any concrete kind
or
- 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.