Demonstrate that higher-order pattern unification is too weak to replace Haskell-style unification

PatternUnificationIsTooWeak.agda

{- I suggested that higher-order pattern unification (as in Agda) might be a viable improvement over Haskell-style unification
for higher-kinded types.

This snippet demonstrates it is not. To this end, I tried to encode something similar similar to this snippet

```
def f[F[_], A](fa: F[A]) = ???
f[type lambda here, ...](Good("winning"): String Or Int)
```
That's taken 
https://github.com/scala/scala/pull/5102#issuecomment-210874674
-}

-- Setup
data Unit : Set where
  unit : Unit

f : ∀ {F : Set → Set} → F Unit → F Unit
f x = x

data G₁ : Set → Set where
data G₂ : Set → Set → Set where

-- Type inference gives up on the applications of f here:
g₁ : G₁ Unit → G₁ Unit
g₁ x = f x

-- and even here:
g₂ : G₂ Unit Unit → G₂ Unit Unit
g₂ x = f x

-- References:
-- pattern unification is explained quickly on pages 3 and 4 of
-- http://homepages.inf.ed.ac.uk/jcheney/publications/cheney05unif.pdf
-- Based on the definitions, it is clear that the term F X (where F and X are metavariables, that is must be inferred)
-- is not a pattern. Worse, even F Unit is not a pattern.