#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