Введите параметр в контексте, который вызывает некоторую двусмысленность

У меня есть следующая ошибка для cadr1 ниже, что имеет смысл

Не удалось вывести (BoolEq n ('Succ ('Succ n'0)) ~ 'True)

из контекста (BoolEq n ('Succ ('Succ n')) ~ 'True)

Переменная типа «n'0» неоднозначна

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE GADTs          #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes     #-}
{-# LANGUAGE TypeFamilies   #-}

module DecidablePropositionalEquality where


data Nat = Zero | Succ Nat

data Vec :: * -> Nat -> * where
  VNil  :: Vec a Zero
  VCons :: a -> Vec a n -> Vec a (Succ n)

type family Greater (a:: Nat) (b:: Nat) :: Bool where
  Greater Zero Zero = True
  Greater Zero (Succ x) = False
  Greater (Succ x) Zero = True
  Greater (Succ a) (Succ b) = Greater a b

op :: forall a n n'. (Greater n (Succ (Succ n')) ~ True) => Vec a n -> a 
op v = undefined

Я не использую n' на сайте определения, так что это неоднозначно.

Могу ли я в любом случае дать экзистенциальную количественную оценку этому n', чтобы ghc не пытался присвоить его какому-либо типу и потерпел неудачу, поскольку ничто не связывает его ни с чем?

В более общем смысле, как контролировать область действия этих переменных типа?

изменить: изменено для удаления семейства логических типов.