app_builder failed

Stream: general

[Hans-Dieter Hiep]

Hi all! I have a question regarding mutual inductive definitions. The following definition:

set_option trace.app_builder true
mutual inductive pexp, farglist (e : tenv self)
with pexp: type α → Type 1
| const (c : constant_name α): pexp (result_type c)
| app (f : function_name α):
    farglist (args_type f) → pexp (result_type f)
| lookup {ty : type α}: rvar e ty → pexp ty
| requal {c : class_name α}:
    pexp (type.ref c) → pexp (type.ref c) → pexp (boolean α)
with farglist: list (type α) → Type 1
| nil: farglist []
| cons {ty : type α} {l : list (type α)}:
    pexp ty → farglist l → farglist (ty::l)

Fails with the message:

[app_builder] failed to create an 'psigma'-application, failed to solve unification constraint for #2 argument (?x_0 → Sort ? =?= type α → Type)

What can I do to resolve this error?

[Hans-Dieter Hiep]

The same error occurs with a smaller definition too:

set_option trace.app_builder true
mutual inductive pexp, farglist (e : tenv self)
with pexp: type α → Type
| const (c : constant_name α): pexp (result_type c)
| app (f : function_name α): pexp (result_type f)
with farglist: list (type α) → Type
| nil: farglist []

[Simon Hudon]

What about the definition of type?

[Hans-Dieter Hiep]

type is an inductive type:

inductive type (α : Type) [names α]
| ref: class_name α → type
| data: record_name α → type

To work around, I have continued the formalisation with the "do it yourself" suggestion of Mario, without using nested/mutual. This works out quite well!

[Floris van Doorn]

The following even smaller example does work for me:

variable {α : Type}
constant type : Type → Type
constant constant_name : Type → Type
constant result_type : constant_name α → type α
noncomputable def function_name := constant_name
constant unknown : Type
constant self : unknown
constant tenv : unknown → Type

set_option trace.app_builder true
mutual inductive pexp, farglist (e : tenv self)
with pexp : type α → Type 1
| const (c : constant_name α): pexp (result_type c)
| app (f : function_name α) : pexp (result_type f)
with farglist: list (type α) → Type 1
| nil: farglist []

Is the type of any of these definitions very different than what you have? I don't know how robust mutual inductive types are, maybe there is a bug there. One thing you might want to double check is whether there is a universe error? Does any of the definitions already land in Type 1 (instead of Type/Type 0)?

[Floris van Doorn]

If it's a bug within the compilation of mutual inductive types, then manually indexing the inductive type over type α ⊕ list (type α) is indeed the way to go, although probably a bit more annoying to work with.

[Floris van Doorn]

Hmm... I can reproduce your error with the following setup:

constant names : Type → Type
attribute [class] names
constant type (α : Type) [names α] : Type
constant constant_name : Type → Type
constant result_type {α : Type} [names α] (c : constant_name α) : type α
noncomputable def function_name := constant_name
constant unknown : Type
constant self : unknown
constant tenv : unknown → Type

variables {α : Type} [names α]
set_option trace.app_builder true
mutual inductive pexp, farglist (e : tenv self)
with pexp: type α → Type
| const (c : constant_name α): pexp (result_type c)
| app (f : function_name α): pexp (result_type f)
with farglist: list (type α) → Type
| nil: farglist []

[Floris van Doorn]

In my last minimal example (where I reproduced the error), I can do another workaround for this mutual inductive type, by giving all arguments to type explicitly:

variables {α : Type} [n : names α]
mutual inductive pexp, farglist (e : tenv self)
with pexp: @type α n → Type
| const (c : constant_name α): pexp (result_type c)
| app (f : function_name α): pexp (result_type f)
with farglist: list (@type α n) → Type
| nil: farglist []

I suspect that this workaround will also work in your case. There indeed seems to be a bug with type class inference in mutual inductive types.

[Hans-Dieter Hiep]

Yes, I have indeed used class instances. Previously, I also encountered a problem with nested inductive definitions. Next time, I will remember to supply all implicit arguments. Thanks a lot, Floris!