#14203: GHC-inferred type signature doesn't actually typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): In comment:6 we have {{{ Foo :: forall a. F a -> * }}} That's an ambiguous kind! Just like for a function {{{ foo :: forall k. F k -> Int }}} is ambiguous. So all uses of `Foo` will give rise to ambiguity. But alas we do not check for ambiguous kinds. Instead we see a "call" of `Foo` in the type signature {{{ bar :: forall a (z :: F a). Foo z -> Int }}} At the use of `Foo` we intantiate `k` to `kappa` and check that `F kappa` is equal o the kind of `z` namely `F a`. So for the type to be well- kinded we need `F kappa ~ F a`. But we have no way to prove that (unless `F` is injective). And that's the error. TL;DR: it's `Foo` that should be rejected as having an ambiguous kind. (I have not studied the oroginal Description; just assuming that comment:6 embodies the essence.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler