Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Adding a type constraint in a checking phase

Email Gateway (Aug 23 2022 at 09:17):

From: Manuel Eberl <eberlm@in.tum.de>
Hello,

I want to write a checking phase that runs at the same stage as type
inference. The purpose of that phase is to constrain the type of certain
constants under certain conditions.

Suppose I encounter a certain constant c during checking with some
polymorphic type attached to it. I now want to add a constraint that
this type conforms to a certain pattern (whose variables are supposed to
be disjoint from everything else in the context).

Error messages arising from this constraint should appear to the user
just like normal type unification errors during type checking.

For instance, if I see a constant "coeff :: 'a poly ⇒ 'b ⇒ 'c", I would
like to unify its type with the pattern "'a list ⇒ nat ⇒ 'a" (after
renaming the variables in the latter).

I see two ways of doing this:

1. add a constraint (using Type.constraint) to the list of terms
2. unify the types manually and propagate the resulting substitution

The first one seems easier to me, although I would probably have to
ensure I don't add constraints that are already there (or can I assume
that by the time my phase is called, all constraints have already been
resolved?).

In both cases, I am not sure what I have to do to make sure the
variables in my type pattern are fresh.

There are probably some established patterns to follow here

Manuel

Last updated: Apr 25 2024 at 16:19 UTC