[GHC] #14203: GHC-inferred type signature doesn't actually typecheck

[GHC]

#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