The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Let me quickly point out at my papers on the matter. Indeed unbox f x ~ 1 triggers unification of unbox f x with 1. How to circumvent it, I will try something asap.

On Sat, Nov 23, 2019 at 9:38 PM Arthur Azevedo de Amorim <arthur.aa AT gmail.com> wrote:

Hi everyone,

I am trying to use canonical structures for an inference task, and I
am having trouble getting the unification engine to cooperate:

From Coq Require Import ssreflect ssrfun.
Set Implicit Arguments.

Record box T := Box { unbox : T }.
Canonical box_def T x := @Box T x.

(* I want Coq to try unify "unbox f ~ S" and "x ~ 0" and to conclude
that "f" must be "box_def S",
  since "box_def" is canonical. But the inference does not work... Maybe the
  first unification problem "unbox f x ~ 1" is triggering the
canonical structure inference directly? *)
Fail Definition infer :=
  (fun (f : box (nat -> nat)) (x : nat) & phant_id (unbox f x) 1 =>
(f, x)) _ _ id.

(* If "unbox" does not appear in head position, unification works just fine. *)
Definition infer :=
  (fun (f : nat -> nat) (x : box nat) & phant_id (f (unbox x)) 1 =>
(f, x)) _ _ id.

Is this behavior intentional? Can it be circumvented?


--
Arthur Azevedo de Amorim