Thanks for your response, I think you helped me on one of my previous abberations.
Hmmm....this all slightly does my head in....on one hand we have types....then type classes (which appear to be a relation defined on types)....then existential types...which now appear not to be treated quite in the same way as 'normal' types....and in this instance the syntax even seems to change....does
"instance Num a => A a"
Mean the same thing as
"instance A (forall a.Num a=>a)"
Uh... that second one is pretty much nonsensical to me. I could imagine it meaning the type (forall a.Num a => a) itself is an instance of A, but not specializations of it (like Int). But without an identity in the type system, the meaning of that would be convoluted. It's kind of off topic, but just for the interested, here are two similar, legal constructions:
ok
Existential: newtype Numeric = forall a. Num a => Numeric a
My compiler doesn't like this...." A newtype constructor cannot have an existential context,"
Universal: newtype Numeric' = Numeric' (forall a. Num a => a)
Not so sure I understand the difference here.....
Both of which are easily declared to be instances of Num. They're not what you want though, because Haskell doesn't support what you want :-(. Anyway, if you have a value of type Numeric, you know it contains some value
of a
Num type, but you don't know what type exactly (and you can never find out). If you have a value of type Numeric', then you can produce a value of any Num type you please (i.e. the value is built out of only operations in the Num class, nothing more specific).
But that was a digression; ignore at your leisure (now that you've already read it :-).
Makes little sense to me...."Numeric" looks reasonable...I think... "Numeric'"...seems weird....and I'm not sure I understood the explanation.
and secondly in what way can this construct lead to "undecidable instances"
Okay, read:
instance A a => B b
(where a and be might be more complex expressions) not as "b is an instance of B whenever a is an instance of A", but rather as "b is an instance of
B,
and using it as such adds a constraint of A a". Let's look at a slightly more complex (and contrived) example:
class Foo a where foo :: a -> a
instance (Foo [a]) => Foo a where foo x = head $ foo [x]
Then when checking the type of the expression foo (0::Int), we'd have to check if Foo Int, Foo [Int], Foo [[Int]], Foo [[[Int]]], ad infinitum.
Ooo blimey....that sort of makes sense.
What are the instances, and what about them is undecidable....seems pretty decidable to me?
What is the ramifications of turning this option on?
Theoretically, compile time fails to guarantee to ever finish. Practically, ghc will give you a very-difficult-to-reason-about message when
constraint
checking stack overflows.
Luke