CODEWITHSUNDEEP
haskell
wind2412
wind2412

Reputation: 1069

Haskell: using ExistentialQuantification and got an error: Couldn't match expected type

I'm using ghc extension ExistentialQuantification and got an error on it. I know the s type of test's second argument's will not be the same as the s defined in test function, but how can I force them to be the same?

1. {-# LANGUAGE ExistentialQuantification #-}
2.
3. data Func = forall s . Func s
4.
5. test :: (s -> a) -> Func -> a
6. test f (Func s) = f s

Got an error:

Untitled..hs:6:21: error:
    • Couldn't match expected type ‘s’ with actual type ‘s1’
      ‘s1’ is a rigid type variable bound by
        a pattern with constructor: Func :: forall s. s -> Func,
        in an equation for ‘test’
        at Untitled..hs:6:9
      ‘s’ is a rigid type variable bound by
        the type signature for:
          test :: forall s a. (s -> a) -> Func -> a
        at Untitled..hs:5:9
    • In the first argument of ‘f’, namely ‘s’
      In the expression: f s
      In an equation for ‘test’: test f (Func s) = f s
    • Relevant bindings include
        s :: s1 (bound at Untitled..hs:6:14)
        f :: s -> a (bound at Untitled..hs:6:6)
        test :: (s -> a) -> Func -> a (bound at Untitled..hs:6:1)

Upvotes: 0

Views: 187

Answers (1)

leftaroundabout
leftaroundabout

Reputation: 120711

The dual to existential quantification (∃) is universal quantification (∀). The dual being needed because the passed-in function has s in contravariant position (i.e. it stands left of the function arrow). Passing a universally-quantified function in as a parameter makes the type of test rank-2, so you need that extension.

{-# LANGUAGE Rank2Types #-}

test :: (forall s . s -> a) -> Func -> a
test f (Func s) = f s

But, note that you won't actually be able to use this in any meaningful way, because the passed in function can't do anything with its argument if if can't know the type. You probably want to add some constraints to both the existential and the universal. Like (I'm using the syntax I'd prefer)

{-# LANGUAGE GADTs, UnicodeSyntax #-}

data Func where
  Func :: Show s => s -> Func

test :: (∀s . Show s => s -> a) -> Func -> a
test f (Func s) = f s

A possibly better alternative is to avoid existential quantification (which is often used in a way that's not really Haskell-idiomatic) entirely, in favour of parametric polymorphism:

data Func s = Func s

test :: (s -> a) -> Func s -> a 
test f (Func s) = f s

Upvotes: 4

Related Questions