Opened 3 years ago

Closed 2 years 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 Rev(s): | ||

Wiki Page: |

### Description (last modified by )

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: 3 Changed 3 years ago by

### comment:2 Changed 3 years ago by

Summary: | Can't match type family with kind polymorphism → 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 follow-up: 4 Changed 3 years ago by

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 follow-up: 5 Changed 3 years ago by

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 Changed 3 years ago by

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 3 years ago by

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:8 Changed 2 years ago by

Description: | modified (diff) |
---|---|

Resolution: | → fixed |

Status: | new → closed |

Test Case: | → indexed-types/should_fail/T9171 |

**Note:**See TracTickets for help on using tickets.

Consider this small variation of your example:

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.