Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://github.com/agda/agda/issues/7753 below:

Coverage checker internal error with copatterns and dot patterns · Issue #7753 · agda/agda · GitHub

The following code results in an internal error:

open import Agda.Builtin.Bool

record Wrap : Set where
  field unwrap : Bool
open Wrap public

data F : Bool → Set where
  c1 : F true
  c2 : F true

G : Bool → Set
G true = Wrap
G false = Bool → Bool

h : (b : Bool) → F b → G b
h true c1 .unwrap = true
h .true c2 .unwrap = true

Error message:

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Coverage/Match.hs:438:19 in Agda-2.8.0-2UHLkJpHripCLhmKYbjPID:Agda.TypeChecking.Coverage.Match

Location of the __IMPOSSIBLE__:

The error stems from matching the split clause false _ _ with the second clause of h.

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4