Internal error for rewriting without --confluence-check

[jespercockx]

(This is a continuation of #3846)

Currently, when you use --rewriting without --confluence-check it is possible to get an internal error, e.g.

{-# 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

We should consider changing this so we get a proper error message when using --rewriting "unsafely".

[jespercockx]

The example I posted above no longer triggers an internal error, and does not actually exploit non-confluence. Here is a better example:

{-# 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

data Unit : Set where
  unit : Unit

postulate
  X : Unit → Set
  X-Nat : X unit ≡ Nat
  X-Bool : (u : Unit) → X u ≡ Bool
{-# REWRITE X-Nat #-}

0' : (u : Unit) → X u
0' unit = 0

{-# REWRITE X-Bool #-}

test : (u : Unit) → not (0' u) ≡ true
test unit = refl

Error:

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Reduce/Fast.hs:1378:20 in Agda-2.6.3-5R57xsQ0HMBLt8bMbFjt5h:Agda.TypeChecking.Reduce.Fast

Error with --no-fast-reduce:

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/CompiledClause/Match.hs:202:9 in Agda-2.6.3-5R57xsQ0HMBLt8bMbFjt5h:Agda.TypeChecking.CompiledClause.Match

[andreasabel]

Cherry-picked onto maint-2.6.2, scheduled for 2.6.2.1