[GHC] #13192: Ambiguity Caused By PolyKind and Not Helpful Error Messages
#13192: Ambiguity Caused By PolyKind and Not Helpful Error Messages -------------------------------------+------------------------------------- Reporter: Shayan-Najd | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Poor/confusing Unknown/Multiple | error message Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The following code results in a confusing/wrong error message, blaming a type variable (`a`) being a fixed Skolem variable: {{{#!hs {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE PolyKinds #-} data I a type family F x type instance F (I a) = a identity :: F (I a) -> F (I a) identity x = x }}} with the error message {{{ • Couldn't match type ‘F (I a0)’ with ‘F (I a)’ Expected type: F (I a) -> F (I a) Actual type: F (I a0) -> F (I a0) NB: ‘F’ is a type function, and may not be injective The type variable ‘a0’ is ambiguous • In the ambiguity check for ‘identity’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature: identity :: F (I a) -> F (I a) | 9 | identity :: F (I a) -> F (I a) | ^^^^^^^^^^^^^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13192 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13192: Ambiguity Caused By PolyKind and Not Helpful Error Messages -------------------------------------+------------------------------------- Reporter: Shayan-Najd | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): To add more information: this code is accepted without `PolyKinds`, because `F (I a)` can immediately reduce to `a`. With `PolyKinds`, `F (I a)` is stuck, as we don't know `a`'s kind. (The equation for `F` works only when `(a :: Type)`.) Perhaps the best fix is to add a check in !TcErrors for type families that match on invisible parameters (i.e., kinds) and emit a {{{NB: Type family `F' has equations that depend on the kind of its argument(s)}}}. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13192#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13192: Ambiguity Caused By PolyKind and Not Helpful Error Messages -------------------------------------+------------------------------------- Reporter: Shayan-Najd | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): Why does it also not work if I change the definition of `F` to {{{ type family F (x :: *) :: k }}} in which case ghci tells me the instance is {{{ type instance F k (I k a) = a -- Defined at I.hs:7:16 }}} but ghc gives the same error regarding `identity`. Is `k` not determined by the result kind of the type family, i.e., the fact that `F (I a)` appears as a type argument to `(->)`? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13192#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13192: Ambiguity Caused By PolyKind and Not Helpful Error Messages -------------------------------------+------------------------------------- Reporter: Shayan-Najd | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Can you explain more precisely why `F (I a)` is stuck with `PolyKinds`? I don't get it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13192#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13192: Ambiguity Caused By PolyKind and Not Helpful Error Messages -------------------------------------+------------------------------------- Reporter: Shayan-Najd | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): In the original program, the application `F (I a)` is stuck because * `data I a` really means `data I k (a :: k) :: *`, i.e., `I` is polykinded * `type family F x` really means `type family F k (x :: *) :: *`, i.e., `F` is ''not'' polykinded * `type instance F (I a) = a` really means `type instance F (I * a) = a`, because the instance is only well-kinded when `a` has kind `*`. But there's nothing stopping one from adding an additional instance `type instance F (I Maybe) = Char` which uses `I` at a different kind. * `identity :: F (I a) -> F (I a)` really means `identity :: forall k (a :: k). F (I k a) -> F (I k a)`, i.e., `identity` is polykinded. Now there's a problem because the instance we defined only applies when `k = *`, but here `k` could really be anything, like `* -> *`. And indeed if I added the `type instance F (I Maybe) = Char`, then I can write `identity @ Maybe` and it has type `Char -> Char` just like `identity @ Char` does. So the type really is ambiguous. What I'm confused about is why `F (I a)` is still stuck even when I make the result of `F` polykinded, so that the instance `type instance F (I a) = a` applies at all kinds. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13192#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13192: Ambiguity Caused By PolyKind and Not Helpful Error Messages -------------------------------------+------------------------------------- Reporter: Shayan-Najd | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): The type instance in @rwbarton's case expands to `F k (I k a) = a`. This instance requires the two `k`s to be the same. In `identity`'s type signature, we get `F (TYPE r) (I k a) -> F (TYPE r') (I k a)`. GHC (rightly) doesn't know that `k` and `TYPE r` are the same. (The fact that it's `TYPE r` and not `Type` is ''not'' the issue.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13192#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13192: Ambiguity Caused By PolyKind and Not Helpful Error Messages -------------------------------------+------------------------------------- Reporter: Shayan-Najd | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: #10789 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: => TypeFamilies * related: => #10789 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13192#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC