Open
Description
@oskeri and I discovered that artifacts of variable generalization arrive at backends in certain cases, e.g. if you compile Relation.Nullary.Decidable of the standard library. Here is the fragment that matters:
module DeadcodeGeneralizedField where
open import Level using (Level)
open import Function.Bundles using (Injection; module Injection)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Definitions using (Decidable)
private
variable
a b ℓ₁ ℓ₂ : Level
open import Relation.Nullary.Decidable.Core
via-injection : {S : Setoid a ℓ₁} {T : Setoid b ℓ₂}
(inj : Injection S T) (open Injection inj) →
Decidable Eq₂._≈_ → Decidable Eq₁._≈_
via-injection inj _≟_ x y = map′ injective cong (to x ≟ to y)
where open Injection injIn the MAlonzo-generated code we see things like:
-- DeadcodeGeneralizedField..generalizedField-a
d_'46'generalizedField'45'a_583 ::
T_GeneralizeTel_591 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'a_583 v0
= case coe v0 of
C_mkGeneralizeTel_593 v1 v2 v3 v4 -> coe v1
_ -> MAlonzo.RTE.mazUnreachableError
...
-- DeadcodeGeneralizedField.GeneralizeTel
d_GeneralizeTel_591 = ()
data T_GeneralizeTel_591
= C_mkGeneralizeTel_593 MAlonzo.Code.Agda.Primitive.T_Level_18
MAlonzo.Code.Agda.Primitive.T_Level_18
MAlonzo.Code.Agda.Primitive.T_Level_18
MAlonzo.Code.Agda.Primitive.T_Level_18Such temporary definitions should not enter the interface file under regular circumstances, meaning in cases where all metavariables could be solved.
They seem to stem from a local open (one of (open Injection inj) and where open Injection inj) but it is unclear why they enter the toplevel.