[GHC] #14131: Difference between newtype and newtype instance

[GHC]

#14131: Difference between newtype and newtype instance
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  patch
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.1
      Resolution:                    |             Keywords:  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #7938, #9574,     |  Differential Rev(s):  Phab:D3872
  #13985                             |
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 > It's also worth noting that ​Phab:D3872 reverses a design decision made
 in #7938 and #9574 to only allow kind variables in the RHSes of associated
 type instances if they're explicitly bound by LHS type patterns.

 I don't think it reverses it.  We just didn't implement it properly.   If
 we wrote out the kind arguments we'd see
 {{{
 class C k where
   data family Nat @k :: k -> k -> Type

 instance C (k -> Type) where
   newtype Nat @(k -> Type) :: (k -> Type) -> (k -> Type) -> Type where
     Nat :: forall k (f::k->Type) (g::k->Type).
            (forall xx. f xx -> g xx) -> Nat @(k->Type) f g
 }}}
 So that `k` certainly is bound on the left, in the (invisible) kind
 pattern.

 > But really, the a is Maybe a is bound by the often-neglected RHS type
 pattern.

 I don't like this language.  There is no "RHS type pattern".  Rather,
 there are invisible kind patterns on the LHS.

 And this matters!  Consider
 {{{
 type family T (a :: Type) :: Type
 type family F :: k

 type instance T Int = Proxy (F :: k)
 }}}
 Now `T` does not have a kind parameter, and that `k` on the RHS of the
 `type instance` really is unbound.  Writing out the kind arguments:
 {{{
 type instance T Int = Proxy @k (F @k)
 }}}
 which is manifestly wrong.

 '''Bottom line''': we can't distinguish the two cases in the renamer.  We
 have to check this in the type checker.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14131#comment:8>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler