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

[GHC]

#14131: Difference between newtype and newtype instance
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  new
        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:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 After tinkering around with this example some more, I realized that the
 problem isn't limited to just data family instances—this affects type
 families across the board. Namely, type families do not implicitly bind
 kind variables that users write in result signatures.

 That is, this type synonym definition is legal:

 {{{#!hs
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE PolyKinds #-}

 type F = (Nothing :: Maybe a)
 }}}

 But this type family instance is not legal:

 {{{#!hs
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeFamilies #-}

 type family   F :: Maybe a
 type instance F = (Nothing :: Maybe a)
 }}}
 {{{
 GHCi, version 8.3.20170816: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Main             ( Bug.hs, interpreted )

 Bug.hs:6:37: error: Not in scope: type variable ‘a’
   |
 6 | type instance F = (Nothing :: Maybe a)
   |                                     ^
 }}}

 I don't see any reason why the latter definition should be rejected. One
 could object that all the type variables in a type family instance must be
 bound on the LHS type patterns. But really, the `a` is `Maybe a` is bound
 by the often-neglected //RHS// type pattern. This is made more evident by
 the fact that tweaking the code to avoid the explicit `Maybe a` kind
 ascription makes it typecheck:

 {{{#!hs
 type instance F = Nothing
 }}}

 However, if you inspect `F` with `:info` in GHCi with the `-fprint-
 explicit-kinds` flag enabled, then you discover that you end up achieving
 the same result in the end:

 {{{
 λ> :set -fprint-explicit-kinds
 λ> :i F
 type family F a :: Maybe a      -- Defined at Bug.hs:5:1
 type instance F a = 'Nothing a  -- Defined at Bug.hs:6:15
 }}}

 Here, it becomes evident that the kind variable `a` in `Maybe a` is being
 implicitly bound. But alas, GHC won't let you write it out explicitly.

 This becomes even more infuriating when dealing with associated type
 instances. For example, I tried to write this:

 {{{#!hs
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeFamilies #-}

 class C k where
   type T :: k

 instance C (Maybe a) where
   type T = (Nothing :: Maybe a)
 }}}
 {{{
 GHCi, version 8.3.20170816: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Main             ( Bug.hs, interpreted )

 Bug.hs:9:3: error:
     The RHS of an associated type declaration mentions ‘a’
       All such variables must be bound on the LHS
   |
 9 |   type T = (Nothing :: Maybe a)
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

 Once again, GHC mistakenly assumes that `a` must be bound in a LHS type
 pattern. But the whole point of `T` is that the instance is determined by
 the RHS type pattern! So as a workaround, I must leave off the explicit
 kind signature.

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