Issue658.agda

-- Andreas, 2012-05-24, issue reported by Nisse
{-# OPTIONS --allow-unsolved-metas #-}
-- {-# OPTIONS -v tc.meta:50 #-}
module Issue658 where

import Common.Level

postulate
  A : Set
  P : A → Set
  Q : (x : A) → P x → Set
  p : (x : A) → P x

record R : Set where
  field
    a : A

r : R
r = {!!}

postulate
  q : Q (R.a r) (p (R.a r))

-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/MetaVars.hs:101

-- The internal error was cause by eta-expanding the frozen meta.
-- Eta-expansion of frozen metas is now allowed.