[GHC] #15583: Treating Constraint as Type when using (type C = Constraint)

[GHC]

#15583: Treating Constraint as Type when using (type C = Constraint)
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.5
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #15412
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This may be similar/same as #15412? I can't get to the latest GHC right
 now. Again the "culprit" is using `type C = Constraint`.

 The code example should not compile, but the error it gives is unexpected.
 If we define the associated type family `Ob_ (cat :: Cat ob) :: ob -> C`
 using `C`

 {{{#!hs
 {-# Language KindSignatures, PolyKinds, DataKinds, TypeInType,
 TypeFamilies, FlexibleInstances #-}

 import Data.Kind

 type T = Type
 type C = Constraint

 type Cat ob = ob -> ob -> T

 class Category_ (cat :: Cat ob) where
   type Ob_ (cat :: Cat ob) :: ob -> C

   id_ :: Ob_ cat a => cat a a

 class    NoCls (a::k)
 instance NoCls (a::k)

 instance Category_ (->) where
   type Ob_ (->) = NoCls

   -- id_ :: NoCls a => (a -> a) -XInstanceSigs
   id_ = ()
 }}}

 the definition of `id_` fails (as we expect), but the expected type (`Ob_
 (->) a -> a -> a`) is wrong:

 {{{#!hs
 $ ghci -ignore-dot-ghci 348.hs
 GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( 348.hs, interpreted )

 348.hs:22:9: error:
     • Couldn't match expected type ‘Ob_ (->) a -> a -> a’
                   with actual type ‘()’
     • In the expression: ()
       In an equation for ‘id_’: id_ = ()
       In the instance declaration for ‘Category_ (->)’
     • Relevant bindings include
         id_ :: Ob_ (->) a -> a -> a (bound at 348.hs:22:3)
    |
 22 |   id_ = ()
    |         ^^
 Failed, no modules loaded.
 Prelude>
 }}}

 If we simply replace `Ob_` with `type Ob_ (cat :: Cat ob) :: ob ->
 Constraint`, the expected type (`a -> a`) matches my intuition:


 {{{
 348.hs:22:9: error:
     • Couldn't match expected type ‘a -> a’ with actual type ‘()’
     • In the expression: ()
       In an equation for ‘id_’: id_ = ()
       In the instance declaration for ‘Category_ (->)’
     • Relevant bindings include id_ :: a -> a (bound at 348.hs:22:3)
    |
 22 |   id_ = ()
    |         ^^
 }}}

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