Internal panic with precompiled module

Description

Consider the file NatCast.lean:

class NatCast (R : Type u) where
  natCast : Nat → R

instance : NatCast Int where
  natCast := sorry

which we precompile by writing in the lakefile

package MyPkg {
   precompileModules := true
}

Then writing

import MyPkg.NatCast

in another file causes

INTERNAL PANIC: executed 'sorry'

We can also reproduce this on the command line with lake env lean OtherFile.lean --load-dynlib=libMyPkg-NatCast.so.

The following code is emitted as an initializer

LEAN_EXPORT lean_object* l_instNatCastInt;
lean_object* lean_sorry(uint8_t);
static lean_object* _init_l_instNatCastInt() {
_start:
{
uint8_t x_1; lean_object* x_2; 
x_1 = 0;
x_2 = lean_sorry(x_1);
return x_2;
}
}

Steps to Reproduce

Expected behavior: No internal panic, import succeeds.

Actual behavior: It fails.

Reproduces how often: 100%

Versions

nightly-2022-07-30

Start by reproducing the failure with NatCast.lean, the lakefile precompileModules setting, and OtherFile.lean using the documented --load-dynlib command. Inspect the generated initializer for l_instNatCastInt and its call to lean_sorry; done means the precompiled module imports successfully without an internal panic.