Exporting code for definitions with the universal quantifier in Isabelle

Question

I’m trying to export code from the Isabelle theorem prover using its code extraction tools. The code I’m trying to extract is based on an integrity constraint that returns a boolean value from a record made up of sets of two different types, plus a set of pairs of these types, like this:

typedecl type_a
typedecl type_b

record my_record =
    aset :: "type_a set"
    bset :: "type_b set"
    pair :: "(type_a × type_b) set"

definition constraint :: "my_record ⇒ bool" where"
    constraint rcd = (∀ a b. (a, b) ∈ pair rcd ⟶ (a ∈ aset rcd ∧ b ∈ bset rcd))"

Here is where I try to extract the code to Haskell and SML files:

export_code constraint
    in SML module_name SML_constraint
    in Haskell module_name haskell_constraint

But when doing so, I get a wellsortedness error, which I think is caused by the type I used not being enumerable? Here’s what it looks like:

Wellsortedness error
(in code equation constraint ?rcd ≡ 
    ∀a b. (a, b) ∈ pair ?rcd ⟶ a ∈ aset ?rcd ∧ b ∈ bset ?rcd):
Type type_a not of sort enum
No type arity type_a :: enum

Notably, the problem goes away if I replace the type_a and type_b types with natural numbers and define a limited value range for them in the constraint, e.g. a maximum of 100:

record my_record =
    aset :: "nat set"
    bset :: "nat set"
    pair :: "(nat × nat) set"

definition constraint :: "my_record ⇒ bool" where
    "constraint rcd = (∀ a < 100. ∀ b < 100. (a, b) ∈ pair rcd ⟶ (a ∈ aset rcd ∧ b ∈ bset rcd))"

For this, the code export works. However, I need to use the abstract types I defined before. Is there a way I can somehow enumerate these types so the error doesn’t occur, or maybe define the constraint in a different way that doesn’t require the ∀ quantifier (which seems to be the cause of the error) but its meaning remains the same?