Re: [isabelle] Restrictions on instance claims



Brendan,

Allowing both

instance
   "*" :: (non_trivial, type) non_trivial
instance
   "*" :: (type, non_trivial) non_trivial

would raise a type inference problem: given a product type 'a * 'b for which
we know that it must be of class non_trivial, there is no most general way to
express this via the classes of the two type variables: either 'a OR 'b need to
be of class non_trivial. Hence Isabelle disallows such "overlapping"
declarations. Sorry. (Not sure what Haskell does these days).

Tobias





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.