On Thu, Jun 26, 2014 at 02:08:24AM -0700, Andras Slemmer wrote:
Your second example shouldn't (and doesn't) compile, as the IsNotFirst instance has an ambiguous variable 'b'. What you want is this 'b' to be existentially quantified and have the compiler provide a witness for it.
That's exactly what I want! Well, modulo actually caring that the witness be provided (of course *that* would raise the 'which one' question). Sorry if that wasn't clear.
Should this compile if we don't have an IsAfter instance in the current module? What if we define one in module B which imports module A? What if we have two IsAfter instances? Which instance should it use?
I understand the general problem of ambiguous types, but my point was that sometimes which instance is picked doesn't matter, and my question was whether there was a way of expressing that - e.g., with a quantifier whose scope doesn't extend to the RHS, so the RHS wouldn't even have access to it. As to the "Should this compile" question, I guess I still don't see how the situation is different from:
v = (undefined::A) t = show v
Which should only compile if there is an instance for Show A. In both cases you need to check whether an instance exists; but in one it's *any* instance, and with the other it's an instance with the right instance head. I concede the former is probably tricky, but I've seen people achieve really tricky things with Haskell types, and have decided to ask even when something looks impossible.
adding extra instance declarations can 'change the truth-value' of the right-hand side.
No, they cannot. instance (IsSecond a) => IsNotFirst a translates to (\forall a. IsSecond(a) -> IsNotFirst(a)), which will always hold. (Unless you switch on overlappinginstances which you shouldnt)
What I meant was that IsNotFirst A, for some concrete A, will hold depending on whether there is an instance declaration - for example, IsNotFirst A. But you're right: without OverlappingInstances, this is a stretch of the imagination, whereas with it, you can have type-level boolean witnesses to this 'change'.