Internal Error in SparseMatrix.hs

[UlfNorell]

From steve.tr...@gmail.com on May 26, 2013 05:40:43

-- agda 2.3.2, stdlib 0.7.

-- Error message: -- An internal error has occurred. Please report this as a bug. -- Location of the error: -- src/full/Agda/Termination/SparseMatrix.hs:269

-- The bug isn't hit if I move "open RawMonad Identity" out of the "where" -- or if I use ⊤ × ⊤ or List ⊤ instead of Vec ⊤ 1.

module Bug where

open import Data.Vec hiding (⊛) open import Data.Unit open import Category.Monad.Identity open import Category.Monad

bug : Vec ⊤ 1 → Vec ⊤ 1 bug ( ∷ ) = ∷ <$> pure tt ⊛ pure [] where open RawMonad IdentityMonad

Original issue: http://code.google.com/p/agda/issues/detail?id=859

[UlfNorell]

From andres.s...@gmail.com on May 25, 2013 21:36:03

I couldn't reproduce the issue using the development versions of Agda and the standard library.

Status: Fixed

[UlfNorell]

From andres.s...@gmail.com on November 11, 2013 06:27:15

Labels: Type-Defect