-- Test pattern unification

import Data.Vect

comp : {A : Type} -> {B : (a : A) -> Type} ->
       {C : (a : A) -> (b : B a) -> Type} ->
       (f : {a : A} -> (b : B a) -> C a b) ->
       (g : (a : A) -> B a) ->
       (a : A) -> C a (g a)
comp f g a = f (g a)

add2 : Nat -> Nat
add2 = comp S S

data Foo = MkFoo
data Bar = MkBar

foo : Foo -> Bar

bar : Bar -> Nat

baz : Foo -> Nat
baz = (comp bar foo)

comp0 : (B : Nat -> Type) -> ((n : Nat) -> B n) -> Int
comp0 _ _ = 0

test00 : Int
test00 = comp0 _ S

comp2 : (B : Nat -> Type) ->
        ((n : Nat) -> (y : B n) -> Int) -> Int
comp2 _ _ = 0

test20 : Int
test20 = comp2 _ dummy
  where
    dummy : (n : Nat) -> Vect n Int -> Int
    dummy _ _ = 0

test03 : Int
test03 = comp0 _ dummy where
    dummy : (n : Nat) -> Int -> Int
    dummy _ = \x => x