class Eq

class Ord < Eq

type a : Ord

op f : forall e : Ord . e -> e

op c : a

. f (f c) = c;

type t : Eq

op b : t

classes

Eq < Type;

Ord < Type

class

Ord < Eq

types

a : Ord;

t : Eq

op b : t

op c : a

op f : forall e : Ord . e -> e

. f (f c) = c

16.3-16.5: ### Hint:

constrain 't : Ord' is unprovable of '(op f : forall e : Ord . e -> e) (op b : t)'

known kinds are: {Eq}

16.3-16.9: ### Hint:

untypeable term (with type: ? _v5_a * ? _v5_a) '(f b, b)'

16.7: *** Error: no typing for 'f b = b'