PruneLHS.agda

-- {-# OPTIONS -v tc.meta:20 #-}
-- Andreas, 2011-04-21
module PruneLHS where

data _≡_ {A : Set}(a : A) : A -> Set where
  refl : a ≡ a

data Bool : Set where true false : Bool

test : let X : Bool -> Bool -> Bool -> Bool
           X = _
       in (C : Set) ->
          (({x y : Bool} -> X x y x ≡ x) ->
           ({x y : Bool} -> X x x y ≡ x) -> C) -> C
test C k = k refl refl
-- by the first equation, X cannot depend its second argument
-- by the second equation, X cannot depend on its third argument