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

3 May 2017


      #12102: “Constraints in kinds” illegal family application in instance (+
documentation issues?)
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by Iceland_jack:

@@ -16,1 +16,2 @@
- Deriving a standalone `Show` instance *without* the constraint works fine
+ Deriving a standalone `Show` instance *without* the constraint `(IsTypeLit
+ a ~ 'True) => ` works fine

New description:

 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 `(IsTypeLit
 a ~ 'True) => ` 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#comment:2
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler

    