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

Internal error when rewriting type constructors #3846

Closed
jespercockx opened this issue Jun 5, 2019 · 0 comments
Assignees
Milestone

Comments

@jespercockx
Copy link
Member

@jespercockx jespercockx commented Jun 5, 2019

This has been known for a while, but lately I have been reconsidering the kind of guarantees one should be able to expect from rewrite rules, and it bothers me that it's so easy to trigger internal errors:

{-# OPTIONS --rewriting #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat

{-# BUILTIN REWRITE _≡_ #-}

not : Bool  Bool
not true = false
not false = true

postulate rew : Nat ≡ Bool
{-# REWRITE rew #-}

0' : Bool
0' = 0

test : not 0' ≡ true
test = refl

Error message:

An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Reduce/Fast.hs:1347

I'm thinking that we should maybe not allow rewrite rules on type constructors by default.

@jespercockx jespercockx added this to the 2.6.1 milestone Jun 5, 2019
@jespercockx jespercockx self-assigned this Jun 5, 2019
jespercockx added a commit that referenced this issue Jun 10, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
1 participant
You can’t perform that action at this time.