
#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