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

3 Nov 2017

      #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 RyanGlScott):

 OK. So what you're saying is that:

 {{{#!hs
 bar :: forall a (z :: F a). Foo z -> Int
 }}}

 Should be rejected as an ambiguous //occurrence// site (which
 `AllowAmbiguousTypes` does not permit) rather than an ambiguous
 //definition// site (which `AllowAmbiguousType` //does// permit)?

 I could buy that, although I'm a bit miffed that there doesn't appear to
 be a satisfying way to resolve the ambiguity. In an ideal world, you could
 say:

 {{{#!hs
 bar :: forall (a :: k) (z :: F @k a). Foo z -> Int
 }}}

 But there's no visible kind application. In a fit of rage, I even tried
 giving kind signatures to //everything//:

 {{{#!hs
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 module Bug where

 type family F (a :: k)
 data Foo (z :: F (a :: k))

 bar :: forall (a :: k) (z :: F (a :: k)). Foo (z :: F (a :: k)) -> Int
 bar _ = 42
 }}}

 But that still produces the same error. So how am I supposed to proceed
 from here?

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203#comment:12
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler