[Haskell-cafe] Quantification in Instance Contexts

[Julian K. Arni]

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'.