Treating Constraint as Type when using (type C = Constraint)
This may be similar/same as #15412 (closed)? 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
{-# 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_ = ()
| ^^