Opened 12 months ago

Closed 6 months ago

#9171 closed bug (fixed)

Clarify error messages when there is a kind mismatch

Reported by: MikeIzbicki Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.8.2
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: indexed-types/should_fail/T9171
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description (last modified by thomie)

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

2) 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.

Change History (8)

comment:1 follow-up: Changed 12 months ago by kosmikus

Consider this small variation of your example:

data Base

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

type instance GetParam Base Int   = Int
type instance GetParam Base Int   = Maybe
type instance GetParam Base Maybe = Bool

test1 = undefined :: GetParam Base (GetParam Base Int :: *)
test2 = undefined :: GetParam Base (GetParam Base Int :: * -> *)

Now test1 has type Int and test2 has type Bool, and the only difference is the intermediate kind of GetParam Base Int which you haven't specified. So I think GHC is right to complain. The kind of the result of GetParam Base Int is ambiguous without annotation, and its choice can in general make a difference.

comment:2 Changed 12 months ago by goldfire

  • Summary changed from Can't match type family with kind polymorphism to Clarify error messages when there is a kind mismatch

kosmikus is right -- kind variables are properly seen as arguments to a type family, and the OP's code is correctly rejected.

However, the error message is quite suboptimal. I wonder if there's a way to detect that kinds are at issue and to suggest -fprint-explicit-kinds (which would make the problem more apparent). As a strawman proposal, we could just look at the rendered output; if the "expected" and "actual" are identical, suggest -fprint-explicit-kinds.

Leaving this ticket open as a request to fine-tune error message.

comment:3 in reply to: ↑ 1 ; follow-up: Changed 12 months ago by MikeIzbicki

Replying to kosmikus:

I was under the impression that type families had to be functions, and so:

type family GetParam (p::k1) (t::k2) :: k3
type instance GetParam Base Int   = Int
type instance GetParam Base Int   = Maybe

would be rejected for having conflicting definitions. If we change the code to:

type family GetParam (p::k1) (t::k2) :: *
type instance GetParam Base Int   = Int
type instance GetParam Base Int   = Double

then the program does get rejected as having conflicting definitions. Is there a good reason to allow the former but not the latter?

comment:4 in reply to: ↑ 3 ; follow-up: Changed 12 months ago by rwbarton

Replying to MikeIzbicki:

The kind of your first GetParam would be forall k3 k1 k2. k1 -> k2 -> k3 meaning that for each triple of kinds (k1,k2,k3), GetParam is a type function k1 -> k2 -> k3. It doesn't mean that for each pair of kinds (k1,k2) there is a kind k3 which is determined by the type family and a type function k1 -> k2 -> k3. It's like the type level forall c a b. C a b c => a -> b -> c (though it's not a perfect analogy; since type families can perform type-level "kind-case" but functions can't perform type-case, I added a type class constraint).

Or, if you convert the polykindedness to extra arguments to the type family (as ghci will show you is happening behind the scenes if you :info GetParam), then your instances become

type instance GetParam * * * Base Int = Int
type instance GetParam (* -> *) * * Base Int = Maybe

and now you can see that they don't conflict.

comment:5 in reply to: ↑ 4 Changed 12 months ago by MikeIzbicki

That makes sense. Was that decision made due to implementation convenience? Or are there examples of type families where we really would want that?

comment:6 Changed 12 months ago by goldfire

I've written several type families where we really do want this behavior. I can't speak to why it was designed to work this way, but I have benefitted from this decision.

One example is to be able to encode overloaded numbers in types:

type family FromNat (n :: Nat) :: k
type instance FromNat n = n        -- identity
type instance FromNat n = ToU n    -- for UnaryNat
type instance FromNat n = ToZ n    -- for Z (integers)

data UnaryNat = Zero | Succ UnaryNat
type family ToU n where
  ToU 0 = Zero
  ToU n = Succ (ToU (n - 1))

data Z = ...
type family ToZ n where ...

I admit that I'm probably in the minority at using this feature, but it is being used. On the other hand, it is a little alarming to most users at first, and it's definitely not the most intuitive feature.

comment:7 Changed 12 months ago by Simon Peyton Jones <simonpj@…>

In 4b4d81a6b97555a8dbeda2e6387ee151af962473/ghc:

Suggest -fprint-explicit-kinds when only kind variables are ambiguous

This was triggered by looking at Trac #9171. See
Note [Suggest -fprint-explicit-kinds] in TcErrors

comment:8 Changed 6 months ago by thomie

  • Description modified (diff)
  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case set to indexed-types/should_fail/T9171
Note: See TracTickets for help on using tickets.