Horrible error message cause by trailing implicit insertion

[UlfNorell]

From andreas....@gmail.com on October 12, 2013 07:25:42

open import Common.Prelude

data ⊥ : Set where record ⊤ : Set where

Zero : Nat → Set Zero 0 = ⊤ Zero (suc _) = ⊥

test : (n : Nat) {p : Zero n} → Set → Set test 0 A = A test (suc _) {()}

-- Horrible error for first clause: -- Cannot eliminate type Set with pattern {(implicit)} (did you supply -- too many arguments?) -- when checking that the pattern zero has type Nat

-- Caused by trailing implicit insertion.

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

[UlfNorell]

From andreas....@gmail.com on October 14, 2013 12:40:41

Turned off trailing implicit insertion. Not needed because of flexible function arity.

Status: Fixed