a.agda

gistfile1.txt

{-# OPTIONS --rewriting #-}
module a where

infix 30 _↦_
postulate
  _↦_ : ∀ {i} {A : Set i} → A → A → Set i

{-# BUILTIN REWRITE _↦_ #-}

data Foo : Set where
  a b c : Foo

data Unit : Set where
  none : Unit

func : Foo → Unit → Foo
func x none = x

alias : (t : Foo) (x : Unit) → Foo
alias t x = func t x

-- This I can do just fine:

-- postulate
--   rw-good : (x : Unit) (t : Foo) → func t x ↦ t
-- {-# REWRITE rw-good #-}

-- But the following fails:

postulate
  rw-bad : (x : Unit) (t : Foo) → alias t x ↦ t
{-# REWRITE rw-bad #-}

-- with error message:

-- rw-bad  is not a legal rewrite rule, since the left-hand side
-- alias t x  reduces to  func t x
-- when checking the pragma REWRITE rw-bad