Opened 2 years ago
Closed 23 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 Rev(s): | ||
Wiki Page: |
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: ↓ 3 Changed 2 years ago by kosmikus
comment:2 Changed 2 years 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: ↓ 4 Changed 2 years 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: ↓ 5 Changed 2 years 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 2 years 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 2 years 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 2 years ago by Simon Peyton Jones <simonpj@…>
comment:8 Changed 23 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
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.