A RetroSearch Logo

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

Search Query:

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

Internal error in generate-helper (C-c C-h) · Issue #7105 · agda/agda · GitHub

Generated-helper under a pattern-let generates an internal error:

open import Agda.Primitive renaming (Set to Type)
open import Agda.Builtin.Sigma

postulate
  ℕ : Type

data T (n : ℕ) : Type where
  conv : ∀ m → T m → T n

test : ∀ n → T n → Σ ℕ T
test n (conv m t) = let n' , t' = test m t in {!helper t'!}  -- C-c C-h

-- An internal error has occurred. Please report this as a bug.
-- Location of the error: impossible, called at src/full/Agda/Interaction/BasicOps.hs:980:49

Error location is pointing to this impossible:

-- Konstantin, 2022-10-23: We don't want to print section parameters in helper type. freeVars <- getCurrentModuleFreeVars contextForAbstracting <- drop freeVars . reverse <$> getContext let escapeAbstractedContext = escapeContext impossible (length contextForAbstracting)

CC @knisht

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