
#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):
Should be rejected as an ambiguous occurrence site (which AllowAmbiguousTypes does not permit) rather than an ambiguous definition site (which AllowAmbiguousType does permit)?
Yes. Precisely like this case: {{{ {-# LANGUAGE AllowAmbiguousTypes #-} f :: F a -> Int -- Ambiguous, but allowed because of the pragma f = e boogle :: F b -> Int boogle v = f v }}} GHC instantiates `F` at `alpha` and then complains it can't equate `F b ~ F alpha`. Visible type application is the solution. The only thing happening in this ticket is that this very same pattern is manifesting at the type level instead of the term level. Nothing more! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler