I want to write a recursive polymorphic function that does one thing for an argument of type ℙ, another thing for an argument of any type other than a function, and the third thing for function arguments. How can I do this?

I thought of two ways:

- Make a type class with overlapping instances. _(Haskell would let me do this.)_
- Make a polymorphic function that takes a type and case splits on it.

Nothing works so far.

The type class approach does not work because Coq does not understand that I want it to try the most specific instance first. Since a function type is also a type, Coq always chooses the most general instance.

The polymorphic function approach does not work because Coq does not let me match on a type:

```
Recursive definition on "Type"
which should be a recursive inductive type.
```

How can I solve this?

Ignat Insarov said:

The type class approach does not work because Coq does not understand that I want it to try the most specific instance first. Since a function type is also a type, Coq always chooses the most general instance.

adjust the instance priority

Reify your type. Instead of having a function `foo: Type -> U`

, have a function `foo: forall {t:T}, eval t -> U`

with `eval: T -> Type`

. Then, you can match on `t`

.

I see, so fixed points require inductive arguments, but _«flat»_ definitions do not, so I can define a flat `eval`

. Nice!

But how do I pattern match a function type?

T is supposed to be an inductive

This does not work:

```
Variant reified_type := reified_any_type | reified_property | reified_function.
Definition reify_type: Type → reified_type := λ type, match type with ℙ => reified_property | x → y => reified_function end.
```

Here `reify_type`

is what Guillaume calls `eval`

.

Error: Invalid notation for pattern.

What he calls `eval`

is the other way around.

`eval : T -> Type`

instead of having something like

```
Inductive is_type : Type -> Type :=
| fun_is_type : forall A B, is_type (A -> B)
...
Definition my_thing T {t : is_type T} := match t with ...
```

you would do

```
Inductive type :=
| fun_type : forall A B : Type, type
...
Definition eval t := match t with
| fun_type A B => A -> B
| ...
```

Ah, so `T`

is `reified_type`

?

I see.

So, it is more like `dematerialize_type`

, or whatever the antonym of _«reify»_ is.

Reification works in that it allows me to case split on the type once. However, I still cannot recurse on it the way I wanted to since the function arrow is not an inductive constructor. But the class based approach also works, as Gaëtan suggested. Thanks to everyone!

Ignat Insarov has marked this topic as resolved.

Last updated: Jan 27 2023 at 02:04 UTC