CODEWITHSUNDEEP
haskelltypestype-kinds
crockeea
crockeea

Reputation: 21811

Equality constraints in Constraint kinds

My question is about how to put an equality constraint in an associated type constraint (i.e. type of kind Constraint)

The specific use case is a class parameterized by a partially applied type:

class Foo c where -- c has kind *->*->*
  type Ctx c m r :: Constraint
  f :: (Ctx c m r) => c m r -> c m r

In a particular instance, I would like to write:

data Bar m r = ...

instance Foo Bar where
   type Ctx Bar m r = (m~Maybe b) 
   -- m must be a Maybe, I don't care what its parameter is
   f = ...

However, GHC complains: 'Not in scope: type variable b'. I don't see any other way to express this constraint. Not every instance requires that 'm~Maybe b', so I cannot move this constraint to the type signature of f. b is not in scope in the instance anywhere (perhaps this is what GHC is complaining about), but there is no need for it to be. The function

f :: (a ~ Maybe b) => a -> a -> a

is valid, I see no reason why I can't do this with Constraints. This problem occurs with top-level constraints, as well as with associated type constraints.

Possibly related is this question, except I need equality with a variable NOT in scope.

Upvotes: 3

Views: 505

Answers (1)

Daniel Wagner
Daniel Wagner

Reputation: 152707

Here is another way to express this constraint:

class IsMaybe m {- where ...whatever operations you need to do on Maybe values -}
instance IsMaybe (Maybe b) {- where ...implement those operations -}
instance Foo Bar where
    type Ctx Bar m r = IsMaybe m

However, given Haskell naming conventions, I would be kind of surprised if this is actually what you want -- is m really a type variable of kind * and not of kind * -> *? In case it's the latter, you'd just want

instance Foo Bar where
    type Ctx Bar m r = m~Maybe

...and possibly a kind annotation in the class declaration for Foo.

Upvotes: 2

Related Questions