-- Andreas, 2012-01-10
-- {-# OPTIONS -v tc.constr.findInScope:50 #-}
module InstanceGuessesMeta where

data Bool : Set where
  true false : Bool

postulate
  D : Bool -> Set
  E : Bool -> Set
  instance d : {x : Bool} -> D x
  f : {x : Bool}{{ dx : D x }} -> E x

b : E true
b = f  -- should succeed
-- Agda is now allowed to solve hidden x in type of d by unification,
-- when searching for inhabitant of D x
