Search code examples
haskelltype-constraints

Constraint to see if one type "satisfies" another

Is there a way to write a constraint:

C t1 t2 :: Constraint

Such that it "satisfies" (is that the right word) if t2 matches against t1.

For example:

C (forall a. Num a => a -> a -> a) (forall a. Num a => a -> a -> a) -- good
C (forall a. Num a => a -> a -> a) (Int -> Int -> Int) -- good
C (forall a. Num a => a -> a -> a) (Bool -> Bool -> Bool) -- fails
C (Int -> Int -> Int) (forall a. Num a => a -> a -> a) -- fails
Solution

  • The basic answer is no. Haskell's type system is predicative: a type variable can only be instantiated to a monotype. So if you had

    class C t u

    or

    type family C t u

    the t and u simply can't be instantiated to the polymorphic types you want to talk about.