Skip to content

Internal error when trying to overflow levels #5705

@ksqsf

Description

@ksqsf

The following code will cause an internal error:

module Test where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)

_ : Set1Set18446744073709551615
_ = refl
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/Utils/Suffix.hs:23:17 in Agd-2.6.2-d23be80f:Agda.Utils.Suffix

Information:

  • Agda version 2.6.2
  • MacOS 12.1

Metadata

Metadata

Assignees

Labels

internal-errorConcerning internal errors of Agdalevelsregression in 2.6.2Regression that first appeared in Agda 2.6.2

Type

No type

Projects

No projects

Milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions