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

25 Feb 2019

      #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/6cce36f83aec33d33545e0ef2135894d22...
 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