#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 goldfire): I don't see how you want GHC to accept `bar`. Let's take this slowly. ``` type family F a ``` So far, so good. ``` data Foo (z :: F a) ``` As Simon points out, `Foo` has an ambiguous kind `forall (a :: Type). F a -> Type`. There's no way to infer the choice of `a` from a usage of `Foo`. GHC does not check for ambiguous kinds (it should, I agree), so this definition is accepted with or without `AllowAmbiguousTypes`. Regardless, you've specified `AllowAmbiguousTypes`, so accepting this conforms to your stated desires. ``` bar :: forall a (z :: F a). Foo z -> Int ``` Now we're in deep trouble. This type mentions `Foo z`. Accordingly, GHC must infer the invisible kind parameter to `Foo`. (You might say "Well, obviously it should be `a`!", but that would be assuming `F` is injective.) So GHC rejects this type signature, as it doesn't know what the invisible kind parameter to `Foo` should be. Note that this is ''not'' the normal ambiguity check that `AllowAmbiguousTypes` disables. This type has an ambiguous type variable; the type itself is not ambiguous. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler