RankNTypes and ScopedTypeVariables leads to illegal polymorphic type that cannot be resolved with QuantifiedConstraints

I am trying to write a function which takes a class instance of my custom class VectorSpace (which has the form class VectorSpace t (n :: Nat) a where) and performs Gaussian elimination on it. Currently the function looks like this:

rowEchelon
    :: ( forall m. KnownNat m
       , forall n. KnownNat n
       , Field a
       , VectorSpace t m a
       , VectorSpace t n a
       )
    => (forall k b. t k b -> Int -> b) -- ^ Indexing function
    -> t m (t n a)  -- ^ Matrix
    -> t m (t n a)  -- ^ Resultant row-echelon matrix
rowEchelon indexFunc = loop 0 0
  where
    loop h k matrix
        | h >= mLen || k >= nLen = matrix
        | otherwise = undefined

    mLen = natVal (Proxy :: Proxy m)
    nLen = natVal (Proxy :: Proxy n)

with the following language extensions:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

However, I'm getting the following error:

• Illegal polymorphic type: forall (m1 :: Nat). KnownNat m1
  A constraint must be a monotype
• In the type signature:
    rowEchelon :: (forall m. KnownNat m,
                   forall n. KnownNat n,
                   Field a,
                   VectorSpace t m a,
                   VectorSpace t n a) =>
                  -- | Indexing function
                  (forall k b. t k b -> Int -> b)
                  -> -- | Matrix
                     t m (t n a)
                     -> -- | Resultant row-echelon matrix
                        t m (t n a)
• Perhaps you intended to use QuantifiedConstraints (typecheck)

But adding QuantifiedConstraints leads to the following warning in the forall m. KnownNat m and forall n. KnownNat n:

This binding for ‘[m or n depending on the line]’ shadows the existing binding

and the following error on mLen and nLen:

• Couldn't match kind ‘*’ with ‘GHC.Num.Natural.Natural’
  When matching types
    proxy0 :: Nat -> *
    Proxy :: * -> *
  Expected: proxy0 [n1 or n2]
    Actual: Proxy n0
• In the first argument of ‘natVal’, namely ‘(Proxy :: Proxy [m or n])’
  In the expression: natVal (Proxy :: Proxy [m or n])
  In an equation for ‘nLen’: nLen = natVal (Proxy :: Proxy [m or n]) (typecheck -Wdeferred-type-errors)

How can I resolve this typing conflict?

I think you want the type:

rowEchelon
    :: forall m n t a . ( KnownNat m
       , KnownNat n
       , Field a
       , VectorSpace t m a
       , VectorSpace t n a
       )
    => (forall k b. t k b -> Int -> b) -- ^ Indexing function
    -> t m (t n a)  -- ^ Matrix
    -> t m (t n a)  -- ^ Resultant row-echelon matrix

The constraint (forall m. KnownNat m) is trying to introduce a higher-rank constraint, but that doesn't really make sense. You don't need (and can't possible guarantee) that every m :: Nat has a KnownNat instance. You just need the m :: Nat at which you're calling the function to be a KnownNat.