search

UlfNorell / agda-prelude

Programming library for Agda
MIT License
120 stars 24 forks source link

inferFunRange failing #43

Closed m0davis closed 8 years ago

m0davis commented 8 years ago

Why does inferFunRange fail in the code below? I expected Agda to report "inferFunRange succeeded (x : A) → F x → Set".

open import Prelude
open import Tactic.Reflection

macro
  test-inferFunRange : Tactic
  test-inferFunRange hole = do
    goal ← inferFunRange hole -|
    typeError ( strErr "inferFunRange succeeded" ∷ termErr goal ∷ [] )

bar : Nat
bar = 0

record R (A : Set) : Set₁ where
  field
    F : A → Set

  foo : (x : A) → F x → Set
  foo = case bar of (λ _ → test-inferFunRange {!!})
  {- Error:
       A → Set !=< Set of type Set₁
       when checking that the expression F has type Set
  -}
UlfNorell commented 8 years ago

This is an Agda bug and not a library issue, so I'm closing this.