Why can't I define this rewrite rule for type elimination of proof-irrelevant disjunctions in Agda

Question

I'm attempting to axiomatize a proof-irrelevant disjunction proposition with type elimination in Agda using the universe of proof-irrelevant propositions. However, when I attempt to define rewrite rules for the computation rules I get an error about a certain variable not being bound. For instance, taking a minimal example, the following code does not compile:

{-# OPTIONS --rewriting --prop #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

module Disjunction where

private variable
  α β : Prop
  A : Set

postulate
  _∨_ : (α : Prop) (β : Prop) → Prop

  inl : α → α ∨ β
  inr : β → α ∨ β
  ∨-rec : (a₁ : α → A) (a₂ : β → A) → ((x : α) (y : β) → a₁ x ≡ a₂ y) → α ∨ β → A
  ∨-rec-inl : {a₁ : α → A} {a₂ : β → A} {h : (x : α) (y : β) → a₁ x ≡ a₂ y} {x : α} → ∨-rec a₁ a₂ h (inl x) ≡ a₁ x

{-# REWRITE ∨-rec-inl #-}

and gives me the error

∨-rec-inl  is not a legal rewrite rule, since the following variables are not bound by the left hand side:  x

However, this error no longer occurs when I change α ∨ β to be a type (i.e. a term of Set) instead of a proof-irrelevant proposition. Why is this?

Answer 1

In order to apply the rewrite rule, Agda needs to infer the value of x, i.e. it needs to match the fourth argument to the pattern inl x. However, if this argument is made irrelevant, then it is not allowed for Agda to inspect it (since this would refute the irrelevance) hence Agda rejects the rule.