Qed fails on typechecking valid proof using native_compute

[chluebi]

Description of the problem

The given code example gives the following error on version 8.19.0:

line 22, characters 0-4:
Error: The recursive definition
"fun _ : BinNums.positive => BinPos.Pos.IsNeg" has type
"BinNums.positive -> BinPos.Pos.mask" while it should be
"BinNums.positive -> BinPos.Pos.mask".

The same proof using cbv or vm_compute works fine. The error gets triggered on the Qed, not the native_compute step.

Triggers both in coq 8.19.0 and the current master branch.

Small Coq file to reproduce the bug

Require Coq.PArith.BinPos.

Definition evil := fun
         k : (Numbers.BinNums.positive -> PArith.BinPos.Pos.mask) ->
             unit =>
       k
          (fix Ffix (x1: Numbers.BinNums.positive) :
               PArith.BinPos.Pos.mask :=
                 PArith.BinPos.Pos.IsNeg
          )
.


Goal evil = evil.
Proof.
  native_compute.
  reflexivity.
Qed. (* Error triggered here *)


(* Alternative reproduction case *)
Definition error := Eval native_compute in evil.

(* Interestingly, this does not trigger any error *)
Eval native_compute in evil.

Version of Coq where this bug occurs

8.19.0

Last version of Coq where the bug did not occur

No response

[SkySkimmer]

It appears to need an auxiliary flle:

baz.v:

Module bar.
Inductive T := A | B : nat -> T | X.
End bar.

Include bar.

test:

Require baz.

Definition car := fix Ffix (x1: unit) : baz.T := baz.X.

Goal car = car.
Proof.
  native_compute.
  reflexivity.
Qed. (* Error triggered here *)

I guess it gets a MutInd.t baz.foo instead of (baz.foo,bar.foo) on one side somehow.

[SkySkimmer]

We call compile_mind_field on baz.T pretending that it's a canonical name
I guess we need something like 609102f + using the delta resolver in translate_field instead of using MutInd.make2 n compile_mind_field.
or use some other way to get the correct kerpair from the user name (can't just lookup in the env because it's not there inside functors)