ImpossiblePrimitive.agda

module ImpossiblePrimitive where

-- minimal self-contained demo of a bug
{-
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Primitive.hs:96:25 in Agda-2.6.3-4SMRUe9PON5ygCFeXLsDJ:Agda.TypeChecking.Primitive
-}

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just : A → Maybe A

{-# BUILTIN MAYBE Maybe #-}

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    prj₁ : A
    prj₂ : B prj₁

-- still the same error with
-- data Σ (A : Set) (B : A → Set) : Set where
  -- _,_ : (x : A) → B x → Σ A B

-- builtin sigma wants universe levels
-- {-# BUILTIN SIGMA Σ #-}

-- if we do provide universe levels AND builtin sigma pragma,
-- all is fixed
{-
open import Agda.Primitive

record Σ {ℓ ℓ′} (A : Set ℓ) (B : A → Set ℓ′) : Set (ℓ ⊔ ℓ′) where
  constructor _,_
  field
    prj₁ : A
    prj₂ : B prj₁

{-# BUILTIN SIGMA Σ #-}
-}

postulate Char : Set
{-# BUILTIN CHAR Char #-}

postulate String : Set
{-# BUILTIN STRING String #-}

primitive
  primStringUncons : String → Maybe (Σ Char (λ _ → String))