Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Rewrite rules shouldn't try to match against _⊔_ #2299

jespercockx opened this issue Nov 9, 2016 · 1 comment


Copy link

@jespercockx jespercockx commented Nov 9, 2016

Currently, rewriting and levels don't play very well together:

{-# OPTIONS --rewriting #-}

postulate _↦_ : ∀ {a} {A : Set a} → A → A → Set

open import Agda.Primitive

  mekker : Level → Level → Set
  moomoo : Level → Set → Set
  rew : (a b : Level) → moomoo (a ⊔ b) (mekker a b) ↦ (Level → Level)

{-# REWRITE rew #-}

works : {a b : Level} → moomoo (a ⊔ b) (mekker a b) → Level
works f = f lzero

fails : {a : Level} → moomoo a (mekker a a) → Level
fails f = f lzero

The problem is that the rew rewrite rule is only triggered when the first argument of moomoo is literally of the form a ⊔ b, ignoring the fact that a plain level a is also definitionally equal to a ⊔ a.

@jespercockx jespercockx self-assigned this Nov 9, 2016

This comment has been minimized.

Copy link
Member Author

@jespercockx jespercockx commented Nov 10, 2016

I fixed this, but the fix may break some existing rewrite rules. In fact, these rewrite rules were already broken since they didn't take into account the additional equalities we have for levels. Feel free to give suggestions if you have a better idea to deal with the interaction between rewriting and levels.

@asr asr added this to the 2.5.2 milestone Dec 12, 2016
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
None yet
2 participants
You can’t perform that action at this time.