[isabelle-dev] type errors when defining subclasses of HOLCF type classes

[Brian Huffman]

Hello all,

I am trying to define some subclasses of the HOLCF classes "cpo" and
"pcpo", but I am having some problems with the "class" command. I want
to define one subclass of "cpo", and a second subclass that inherits
from both "pcpo" and the first subclass. I've pasted in a simplified
example to show what the problem is.

theory Test imports HOLCF begin

default_sort cpo

class foo = cpo +
  fixes foo :: "'a → 'a"

class bar = foo + pcpo +
  assumes "foo⋅⊥ = ⊥"

The definition of class "bar" is rejected with this error message:

*** Type unification failed: Variable 'a::type not of sort cpo
***
*** Failed to meet type constraint:
***
*** Term:  below∷'a∷type ⇒ 'a∷type ⇒ bool :: 'a∷type ⇒ 'a∷type ⇒ bool
*** Type:  ??'a∷cpo ⇒ ??'a∷cpo ⇒ bool
***
*** At command "class"

For the next try, I removed the "cpo" and "pcpo" from the list of
superclasses, and put them as annotations on the type variables
instead, which I believe is a supported feature.

class foo2 =
  fixes foo2 :: "'a::cpo → 'a"

class bar2 = foo2 +
  assumes "foo2⋅(⊥::'a::pcpo) = ⊥"

The definition of the second typeclass still fails, but with a
different error message this time:

*** Type unification failed: Variable 'a::pcpo not of sort foo2
***
*** Failed to meet type constraint:
***
*** Term:  foo2 :: ??'a∷foo2 → ??'a∷foo2
*** Type:  'a∷pcpo → 'a∷pcpo
***
*** At command "class"

As a test, I tried changing the annotation from "cpo" to "pcpo" on the
first typeclass, so the annotations match.

class foo3 =
  fixes foo3 :: "'a::pcpo → 'a"

class bar3 = foo3 +
  assumes "foo3⋅(⊥::'a::pcpo) = ⊥"

 Now both class declarations work, although these are not the classes
I wanted to define -- I don't want foo to be a subclass of pcpo.

Finally, I came across a solution that almost does what I want. In the
second class declaration, I annotated the type variable with a class
constraint for the first class:

class foo4 =
  fixes foo4 :: "'a::cpo → 'a"

class bar4 = foo4 +
  assumes "foo4⋅(⊥::'a::{pcpo,foo4}) = ⊥"

So far so good. But then I ran into problems later when I tried to
instantiate the classes:

instantiation unit :: bar4
begin

definition "foo4 = (ID :: unit → unit)"

instance
apply default

At this point, I would expect to have the subgoal "foo4⋅⊥ = ⊥". But
instead, this is what I get:

proof (prove): step 1

goal (1 subgoal):
 1. class.bar4 TYPE(unit)

I then tried "unfolding class.bar4_def", but it does nothing. At this
point in the proof, I only have "unit::pcpo", but theorem
class.bar4_def has "{pcpo,foo4}" as a class constraint.

The only workaround that I could find was to instantiate each class
one at a time, like this:

instantiation unit :: foo4 begin
definition "foo4 = (ID :: unit → unit)"
instance ..
end
instance unit :: bar4
apply default
by (simp add: foo3_unit_def)

And now, finally, the instance proof works correctly. But this seems
to be quite unsatisfactory; the class mechanism is supposed to let us
instantiate a whole collection of classes at once, and not force us to
treat every superclass individually. Imagine if in order to show "rat
:: ordered_field" we had to first provide a separate instance for each
class it derives from!

Anyway, it seems that the only reason the original class definitions
failed is because in addition to the actual typeclasses "foo" and
"bar", the "class" command is also trying to define locale predicates
"class.foo" and "class.bar". I have absolutely no need for such locale
predicates, and I certainly never plan on doing any locale
interpretations for any HOLCF typeclasses. Is there any way to turn
this feature off, then? Or is there some other important reason why
these locales need to exist? I would guess not, since HOLCF used to
work just fine with the old-style "axclass" command.

If it is not possible to turn off the generation of locale predicates,
then at least it seems that the definition of classes foo2/bar2 could
be made to work. In this case, the locale predicates could have class
constraints of "cpo" and "pcpo", as appropriate.

- Brian