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

30 Aug 2018

      #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