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

[GHC]

#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:
                                     |  typecheck/should_fail/T12102
      Blocked By:                    |             Blocking:
 Related Tickets:  #13780, #15872    |  Differential Rev(s):  Phab:D5397
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * status:  closed => new
 * resolution:  fixed =>
 * milestone:  8.8.1 =>


Comment:

 Commit
 [https://gitlab.haskell.org/ghc/ghc/commit/6cce36f83aec33d33545e0ef2135894d22dff5ca
 6cce36f83aec33d33545e0ef2135894d22dff5ca] (`Add AnonArgFlag to FunTy`)
 added back the ability to have equality constraints in kinds.
 Unfortunately, the issues in the original description persist. Here's one
 example of the bizarre things that equality constraints in kinds cause:

 {{{#!hs
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeFamilies #-}
 module T12102 where

 import Data.Kind
 import GHC.TypeLits

 type family IsTypeLit a where
   IsTypeLit Nat    = 'True
   IsTypeLit Symbol = 'True
   IsTypeLit a      = 'False

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

 deriving instance Show (T a)
 }}}
 {{{
 $ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs
 [1 of 1] Compiling T12102           ( Bug.hs, Bug.o )

 Bug.hs:21:25: error:
     • Expecting one more argument to ‘T a’
       Expected a type, but ‘T a’ has kind ‘a0 -> *’
     • In the first argument of ‘Show’, namely ‘(T a)’
       In the stand-alone deriving instance for ‘Show (T a)’
    |
 21 | deriving instance Show (T a)
    |                         ^^^

 Bug.hs:21:27: error:
     • Couldn't match kind ‘*’ with ‘Constraint’
       When matching kinds
         k0 :: *
         IsTypeLit a0 ~ 'True :: Constraint
       Expected kind ‘IsTypeLit a0 ~ 'True’, but ‘a’ has kind ‘k0’
     • In the first argument of ‘T’, namely ‘a’
       In the first argument of ‘Show’, namely ‘(T a)’
       In the stand-alone deriving instance for ‘Show (T a)’
    |
 21 | deriving instance Show (T a)
    |                           ^
 }}}

 Huh? Why is GHC claiming that `T a` has kind `a0 -> *`? Well, if you ask
 GHCi:

 {{{
 λ> :k T
 T :: (IsTypeLit a ~ 'True) -> a -> *
 }}}

 Yikes. Something is clearly wrong here.

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