Re: [isabelle] Restrictions on instance claims
"*" :: (non_trivial, type) non_trivial
"*" :: (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).
This archive was generated by a fusion of
Pipermail (Mailman edition) and