Opened 4 months ago

Closed 4 months ago

#15583 closed bug (duplicate)

Treating Constraint as Type when using (type C = Constraint)

Reported by: Iceland_jack Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.5
Keywords: TypeInType Cc:
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 (last modified by Iceland_jack)

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

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

Change History (2)

comment:1 Changed 4 months ago by Iceland_jack

Description: modified (diff)

comment:2 Changed 4 months ago by RyanGlScott

Resolution: duplicate
Status: newclosed

Yep, this is a duplicate of #15412. Now that that's been fixed, you get the error message you'd expect on the original program:

$ /opt/ghc/8.6.1/bin/ghci Bug.hs
GHCi, version 8.6.0.20180823: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.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 Bug.hs:22:3)
   |
22 |   id_ = ()
   |         ^^
Note: See TracTickets for help on using tickets.