4

Per What are skolems?, this works:

{-# LANGUAGE ExistentialQuantification #-}

data AnyEq = forall a. Eq a => AE a

reflexive :: AnyEq -> Bool
reflexive (AE x) = x == x

But why doesn't this:

reflexive2 :: AnyEq -> Bool
reflexive2 ae = x == x
  where
  AE x = ae

(or the similar version with let). It produces the errors including:

Couldn't match expected type ‘p’ with actual type ‘a’
        because type variable ‘a’ would escape its scope
      This (rigid, skolem) type variable is bound by
        a pattern with constructor: AE :: forall a. Eq a => a -> AnyEq,
        in a pattern binding
        at Skolem.hs:74:4-7

Is it possible to make it work by adding some type declaration (a bit like the s :: forall a. I a -> String solution to the withContext example in that question). I feel I want to add an Eq x somewhere.

My (possibly naïve) understanding of how reflexive works is as follows:

  • it takes a value of type AnyEq. This has embedded within it a value of any type provided it is an instance of Eq. This inner type is not apparent in the type signature of reflexive and is unknown when reflexive is compiled.
  • The binding (AE x) = ae makes x a value of that unknown type, but known to be an instance of Eq. (So just like the variables x and y in myEq :: Eq a => a -> a -> Bool; myEq x y = x == y)
  • the == operator is happy based on the implied class constraint.

I can't think why reflexive2 doesn't do the same, except for things like the "monomorphism restriction" or "mono local binds", which sometimes make things weird. I've tried compiling with all combinations of NoMonomorphismRestriction and NoMonoLocalBinds, but to no avail.

Thanks.

David
  • 309
  • 1
  • 9
  • Consider the general extraction function for `AE`: `openAE f (AE x) = f x; openAE :: (forall a . Eq a => a -> r) -> AE -> r`. When you write `AE x = ae` - it's like trying to write `openAE id`. The type of `id` - `forall a . a -> a` is not compatible with the type `forall a . Eq a => a -> r`. However, writing `(AE x) = x == x` is like writing `openAE (\x -> x == x)` - the type of that function is `forall a . Eq a => Bool` which **is** compatbile with type `forall a . Eq a => a -> r`. – user2407038 Jul 27 '20 at 16:51
  • 1
    @RobinZigmond sure there are values of this type. It's an existential, not a universal. `AE "foo"` will do. – leftaroundabout Jul 27 '20 at 16:54
  • @leftaroundabout oops, thanks for pointing that out, I definitely get confused by Existentials, and just proved it! – Robin Zigmond Jul 27 '20 at 17:02
  • @user2407038 Thanks for your comment (which I'm still trying to understand). I guess I had been assuming that parameters of functions (and case statements) and variables declared in let/where statements worked in much the same way as each other. I guess they don't, as illustrated by more simple examples `case AE 7 of AE x -> x == x` (works) and `let AE x = AE 7 in x` (doesn't). Is there some simple way (or documentation) to help me first understand this difference? Thanks. – David Jul 27 '20 at 17:45
  • Ugh: second example should be `let AE x = AE 7 in x == x` – David Jul 27 '20 at 17:51
  • 2
    I think this is closely connected to [this answer of mine](https://stackoverflow.com/a/23540431/3234959). A major issue here is that `let` pattern matching is lazy (irrefutable), so after the `in` we do not yet have evaluated `AE 7` nor we have an `Eq` dictionary around. We could in principle force the evaluation as soon as the dictionary is demanded but it'd be a rather weird semantics, in the general case. `case AE 7 of ~(AE x) -> x == x` should similarly fail. So far, the general rule to bring in scope class constraints from GADTs is: use strict pattern matching. – chi Jul 27 '20 at 19:22
  • 1
    related: https://stackoverflow.com/questions/53346318/pattern-bindings-for-existential-constructors – Hans Lub Jul 27 '20 at 19:56
  • @chi Yes, I now read the [spec](https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-440003.12), which indeed shows *let p = e1 in e0 = case e1 of ~p -> e0*, with the dreaded ~. So that explains why the two cases are different. (Slightly confusingly, `case AE 7 of ~(AE x) -> x == x` gives a different error: `An existential or GADT data constructor cannot be used inside a lazy (~) pattern`. Maybe some slightly different translation logic for a let with an existential types? But I'll not worry about that right now). – David Jul 28 '20 at 16:36
  • @user2407038 I think I understand your main point: the type of `openAE id` (if it could exist) would have to be `AnyEq -> a` which would be required to return both an (unknown) type from within the AE, but also any type the caller cared to request. (Or maybe it "should" be `Eq a => AnyEq -> a`, somehow preserving the Eq, but still not actually possible.) If we really wanted to do something like that, we should probably declare AnyEq without the existential quantification, and could then write functions with types `AnyEq a -> a`. – David Jul 28 '20 at 17:19
  • @HansLub thanks - I agree this is the same. – David Jul 28 '20 at 17:21
  • However, `let AE x = AE 7 in x == x` certainly doesn't look like it's trying to leak the type of the AE anywhere. It looks (to me) just like `openAE (\x -> x == x)` or `unfoo` (or `reflexive`), so I guess I find it a bit weird that the let translation translates it in a way I didn't really want and that makes it break. (Maybe if/when I figure out the benefit of the ~ in the let translation I'll be happy it's there!). – David Jul 28 '20 at 17:26
  • Your case looks reasonable, but I guess you have to consider the general case to see why GHC does not accept it. E.g. `data IsEq a where E :: Eq a => a -> IsEq a` after which one could write `foo :: IsEq a -> a -> a -> Bool ; foo pr x y = let E z = pr in x==y`. The last `let` is very weird: it defines `z` which is unused, so we would expect that `pr` is not evaluated (laziness). Yet, `x==y` needs the `==` function which comes from the `Eq a` constraint, and that requires evaluating `pr`. Understanding what gets evaluated becomes _very_ tricky. – chi Jul 28 '20 at 17:43
  • Worse, consider this: `foo :: IsEq a -> IsEq a -> a -> a -> Bool ; foo pr1 pr2 x y = let E z = pr1 ; E w = pr2 in x==y`. Which one gets evaluated? `pr1`? `pr2`? Both? If we call `foo (E True) undefined False True` do I get `False` as a result, or an exception? What if we swap the first two arguments? The semantics here is so unpredictable that it becomes quite ugly, IMO. – chi Jul 28 '20 at 17:47
  • @chi thanks for these. I reworked the 2nd example into a case, and this has helped me understand better what is happening. The let translates to `case pr1 of ~(E z) -> case pr2 of ~(E w) -> x == y`, which does not compile (as expected, "no instance of Eq..."). Remove either or both ~ and it compiles (and you can pass `undefined` for the ~ patterns, as expected). So I guess the point of translating let to a version with a ~ is to increase lazyness. The downside is that in some cases type inference doesn't work. And if you'd prefer type inference to lazyness, use case (or similar), not let. – David Jul 29 '20 at 07:08
  • So, overall, I think there are (at least) two different issues here: (1) whether type inference can work (and we see the let statement, which translates to a case with a ~ sometimes precludes that); and (2) whether there is "scope leakage" (as in the `openAE id` example). I think the original `reflexive2` example had type inference issues (which can be fixed by rewriting as a case without a ~), but not scope leakage issues. Yet the error message is about scope leakage, not "no instance of Eq". So, I think there is still something I don't fully understand. – David Jul 29 '20 at 07:17
  • @David `AnyEq -> a` is not quite right - in Haskell syntax this means `forall a . AnyEq -> a`. This is a function which takes an `AnyEq` and returns a value of any type that the caller requests; such a type is uninhabited. In some hypothetical type system, you could claim that `openAE id` has type `AnyEq -> (exists a . Eq a => a)` ; but, `AnyEq` is isomorphic to `exists a . Eq a => a` in such a type system. Indeed, in Haskell, the way you write `exists a . Eq a => a` is by defining a data type like `AnyEq`. – user2407038 Jul 29 '20 at 15:50
  • @user2407038 Hi yes, I think we're both agreeing that `openAE id` is not possible (though in slightly different words). Having looked again at your original answer, I also agree that you can't pass `id :: forall a. a -> a` to something expecting a `forall a . Eq a => a -> r` (hence they're incompatible, as you say). But I also don't see how `reflexive2` is "like" `openAE id`. Rewritten as `let AE x = ae in x == x` seems to translate to `case ae of ~(AE x) -> x == x` which fails but `case ae of AE x -> x == x` is OK. Is the former "like" `openAE id` but the latter not somehow? – David Jul 30 '20 at 09:30
  • Anyway, the good news is I understand some of the issues well enough to progress my coding, even though there are (in my mind) some outstanding questions here. – David Jul 30 '20 at 09:31

1 Answers1

3

So I think I found the answer in the documentation (of all places!). This states:

  • You can’t pattern-match on an existentially quantified constructor in a let or where group of bindings
  • The reason for this restriction is really an implementation one
  • We’ll see how annoying it is

There's also a request to lift the restriction (though it seems a bit challenging).

Personally, now I think I understand it, it's not that annoying. But I do think the error message generated is misleading (since I don't think the problem is scope leakage), so will request it is changed. (It would also be good if the generated error message had a reference back to the documentation, so will push my luck by asking for that too.)

Thanks all for your comments, and please let me know if you think I've got some of this wrong. David.

David
  • 309
  • 1
  • 9
  • “since I don't think the problem is scope leakage” – agree that this isn't a problem in this particular example, though it is in similar ones. – leftaroundabout Jul 30 '20 at 10:33
  • Agreed. There is already an [issue](https://gitlab.haskell.org/ghc/ghc/-/issues/15991) to fix the error message, so I've added a comment there. – David Jul 30 '20 at 10:55