[GHC] #12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?)

22 May 2016

      #12102: “Constraints in kinds” illegal family application in instance (+
documentation issues?)
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 GHC 8.0.0.20160511. Example from the user guide:
 [https://downloads.haskell.org/~ghc/8.0.1/docs/html/users_guide/glasgow_exts....
 #constraints-in-kinds Constraints in kinds]

 {{{#!hs
 type family IsTypeLit a where
   IsTypeLit Nat    = 'True
   IsTypeLit Symbol = 'True
   IsTypeLit a      = 'False

 data T :: forall a. (IsTypeLit a ~ 'True) => a -> * where
   MkNat    :: T 42
   MkSymbol :: T "Don't panic!"
 }}}

 Deriving a standalone `Show` instance *without* the constraint works fine

 {{{#!hs
 deriving instance Show (T a)
 }}}

 but I couldn't define a `Show` instance given the constraints:

 {{{#!hs
 -- • Couldn't match expected kind ‘'True’
 --               with actual kind ‘IsTypeLit a0’
 --   The type variable ‘a0’ is ambiguous
 -- • In the first argument of ‘Show’, namely ‘T a’
 --   In the stand-alone deriving instance for ‘Show (T a)’
 deriving instance Show (T a)
 }}}

 let's add constraints

 {{{#!hs
 -- • Couldn't match expected kind ‘'True’
 --               with actual kind ‘IsTypeLit lit’
 -- • In the first argument of ‘Show’, namely ‘T (a :: lit)’
 --   In the instance declaration for ‘Show (T (a :: lit))’
 instance IsTypeLit lit ~ 'True => Show (T (a :: lit)) where
 }}}

 let's derive for a single literal

 {{{#!hs
 -- • Illegal type synonym family application in instance:
 --     T Nat
 --       ('Data.Type.Equality.C:~
 --          Bool
 --          (IsTypeLit Nat)
 --          'True
 --          ('GHC.Types.Eq# Bool Bool (IsTypeLit Nat) 'True <>))
 --       42
 -- • In the stand-alone deriving instance for ‘Show (T (42 :: Nat))’
 deriving instance Show (T (42 :: Nat))
 }}}

 same happens with

 {{{#!hs
 instance Show (T 42) where
 }}}

 ----

 The documentation
...
Note that explicitly quantifying with `forall a` is not necessary here.
seems to be wrong since removing it results in

 {{{
 tVDv.hs:10:17-18: error: …
     • Expected kind ‘a’, but ‘42’ has kind ‘Nat’
     • In the first argument of ‘T’, namely ‘42’
       In the type ‘T 42’
       In the definition of data constructor ‘MkNat’
 Compilation failed.
 }}}

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12102
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler