[GHC] #9171: Can't match type family with kind polymorphism
#9171: Can't match type family with kind polymorphism ----------------------------+---------------------------------------------- Reporter: | Owner: MikeIzbicki | Status: new Type: bug | Milestone: Priority: normal | Version: 7.8.2 Component: Compiler | Operating System: Unknown/Multiple Keywords: | Type of failure: GHC rejects valid program Architecture: | Test Case: Unknown/Multiple | Blocking: Difficulty: Unknown | Blocked By: | Related Tickets: | ----------------------------+---------------------------------------------- Create a module with the following code: {{{ 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9171 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9171: Can't match type family with kind polymorphism ----------------------------------------------+---------------------------- Reporter: MikeIzbicki | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9171#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9171: Clarify error messages when there is a kind mismatch ----------------------------------------------+---------------------------- Reporter: MikeIzbicki | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (by goldfire): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9171#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9171: Clarify error messages when there is a kind mismatch ----------------------------------------------+---------------------------- Reporter: MikeIzbicki | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (by MikeIzbicki): Replying to [comment:1 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9171#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9171: Clarify error messages when there is a kind mismatch ----------------------------------------------+---------------------------- Reporter: MikeIzbicki | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (by rwbarton): Replying to [comment:3 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9171#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9171: Clarify error messages when there is a kind mismatch ----------------------------------------------+---------------------------- Reporter: MikeIzbicki | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9171#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9171: Clarify error messages when there is a kind mismatch ----------------------------------------------+---------------------------- Reporter: MikeIzbicki | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9171#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9171: Clarify error messages when there is a kind mismatch
----------------------------------------------+----------------------------
Reporter: MikeIzbicki | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.8.2
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
Type of failure: GHC rejects valid program | Unknown/Multiple
Test Case: | Difficulty: Unknown
Blocking: | Blocked By:
| Related Tickets:
----------------------------------------------+----------------------------
Comment (by Simon Peyton Jones
participants (1)
-
GHC