[Haskell-cafe] Quantification in Instance Contexts
Julian K. Arni
jkarni at gmail.com
Thu Jun 26 13:59:38 UTC 2014
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
> > 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
More information about the Haskell-Cafe