Issue383.agda

-- Andreas, 2011-05-09
-- {-# OPTIONS -v tc.meta:15 -v tc.inj:40 #-}
module Issue383 where

data D (A : Set) : A → Set where

data Unit : Set where
  unit : Unit

D′ : (A : Set) → A → Unit → Set
D′ A x unit = D A x

postulate
  Q : (A : Set) → A → Set
  q : (u : Unit) (A : Set) (x : A) → D′ A x u → Q A x

  A : Set
  x : A
  d : D A x

  P : (A : Set) → A → Set
  p : P (Q _ _) (q _ _ _ d)

-- SOLVED, WORKS NOW.
-- OLD BEHAVIOR:
-- Agda does not infer the values of the underscores on the last line.
-- Shouldn't constructor-headedness come to the rescue here? Agda does
-- identify D′ as being constructor-headed, and does invert D′ /six
-- times/, but still fails to infer that the third underscore should
-- be unit.

{-
blocked _41 := d
     by [(D A x) =< (D′ _39 _40 _38) : Set]
blocked _42 := q _38 _36 _40 _41
     by [_40 == _37 : _36]
-}