attempt to use DataKinds

Foo.hs

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE UndecidableInstances #-}
module Foo where

import Prelude hiding ((-))

import GHC.TypeLits (Nat, type (-), type (<=))
import Data.Proxy (Proxy(Proxy))

class Foo (n :: Nat) x y | n x -> y, x y -> n where
  foo :: Proxy n -> x -> y

instance Foo 0 (x,a) x where
  foo _ (x,_) = x

reduce :: Proxy n -> Proxy (n - 1)
reduce _ = Proxy

instance (Foo (n - 1) x y, 1 <= n) => Foo n (a,x) y where
  foo n (_,x) = foo (reduce n) x

-- > :l Foo
-- *Foo> :set -XDataKinds
-- *Foo> foo (Proxy :: Proxy 0) ("",(2::Int,True))
-- ""
-- *Foo> foo (Proxy :: Proxy 1) ("",(2::Int,True))
-- 2
-- *Foo> foo Proxy ("",(2::Int,True)) :: String
-- ""
-- *Foo> foo Proxy ("",(2::Int,True)) :: Int
-- 2
-- *Foo> foo Proxy ("",(2::Int,("a",()))) :: String
-- ""
-- *Foo> foo (Proxy :: Proxy 2) ("",(2::Int,("a",()))) :: String
-- "a"

But:

*Foo> foo Proxy ((1,(2,3)) :: (Int,(Int,Int))) :: Int

<interactive>:28:1:
    Couldn't match type ‘1 GHC.TypeLits.<=? n0’ with ‘'True’
    The type variable ‘n0’ is ambiguous
    In the expression:
        foo Proxy ((1, (2, 3)) :: (Int, (Int, Int))) :: Int
    In an equation for ‘it’:
        it = foo Proxy ((1, (2, 3)) :: (Int, (Int, Int))) :: Int

PS: version 2 suddenly works