Internal error when attempting to prove sqrt2

From jwieg...@gmail.com on October 07, 2013 19:17:51

What's the problem? Cut-and-pasted program examples are preferred over attachments (if reasonably short). module Theorem where

open import Data.Nat
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

0≡n*m : ∀ n → 0 ≡ n * n → n ≡ 0
0≡n*m zero h = refl
0≡n*m (suc n) ()

sqrt2 : ∀ n m → n * n ≡ 2 * m * m → m ≡ 0
sqrt2 zero m p = 0≡n*m m {!!}
sqrt2 (suc n) m p = {!!}

The output I see when trying to load this file is:

An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Records.hs:216 What version of Agda are you using? On what operating system (if relevant)? 2.3.2.1 on OS X 10.8.5

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

UlfNorell / agda-test

Internal error when attempting to prove sqrt2 #916