[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
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #15412            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by Iceland_jack:

Old description:

> 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_ = ()
>    |         ^^
> }}}

New description:

 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:

 {{{
 $ 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#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler