TypeInstantiations.dfy(33,7): Error: an opaque type declaration (B) in a refining module cannot replace a more specific type declaration in the refinement base
TypeInstantiations.dfy(36,13): Error: a type declaration that requires equality support cannot be replaced by a codatatype
TypeInstantiations.dfy(40,7): Error: opaque type 'G' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 0)
TypeInstantiations.dfy(41,7): Error: opaque type 'H' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 2)
TypeInstantiations.dfy(42,7): Error: opaque type 'J' is not allowed to be replaced by a type that takes a different number of type parameters (got 0, expected 1)
TypeInstantiations.dfy(51,8): Error: opaque type 'R' is not allowed to be replaced by a type that takes a different number of type parameters (got 0, expected 1)
TypeInstantiations.dfy(53,8): Error: opaque type 'T' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 0)
TypeInstantiations.dfy(55,7): Error: type 'TP0' is not allowed to change its number of type parameters (got 1, expected 0)
TypeInstantiations.dfy(56,7): Error: type 'TP1' is not allowed to change its number of type parameters (got 0, expected 1)
TypeInstantiations.dfy(34,11): Error: type 'C' is used to refine an opaque type with equality support, but 'C' does not support equality
TypeInstantiations.dfy(35,7): Error: type 'D' is used to refine an opaque type with equality support, but 'D' does not support equality
TypeInstantiations.dfy(48,7): Error: type 'N' is used to refine an opaque type with equality support, but 'N' does not support equality
12 resolution/type errors detected in TypeInstantiations.dfy