Hello everyone, I'm running into a type error I don't quite understand why it's happening. Consider this type class and function: ``` class KnownNat n => F (n :: Nat) foo :: forall n. F n => (F n => Proxy n -> Proxy n) -> Int foo f = let _ = f (Proxy @n) in 0 ``` This typechecks with no issues. But once I add an LTE constraint to the type class it won't typecheck  and complains about an untouchable type. ``` class (KnownNat n, 1 <= n) => F (n :: Nat) foo :: forall n. F n => (F n => Proxy n -> Proxy n) -> Int foo f = let _ = f (Proxy @n) in 0 ``` with this error: ``` test.hs:11:8: error:     • Could not deduce (F n0)       from the context: F n         bound by the type signature for:                    foo :: forall (n :: Nat). F n => (F n => Proxy n -> Proxy n) -> Int         at test.hs:11:8-58       The type variable ‘n0’ is ambiguous     • In the ambiguity check for ‘foo’       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes       In the type signature:         foo :: forall n. F n => (F n => Proxy n -> Proxy n) -> Int     | 111 | foo :: forall n. F n => (F n => Proxy n -> Proxy n) -> Int     |        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ test.hs:11:8: error:     • Couldn't match type ‘n0’ with ‘n’         ‘n0’ is untouchable           inside the constraints: F n0           bound by a type expected by the context:                      F n0 => Proxy n0 -> Proxy n0           at test.hs:11:8-58       ‘n’ is a rigid type variable bound by         the type signature for:           foo :: forall (n :: Nat). F n => (F n => Proxy n -> Proxy n) -> Int         at test.hs:11:8-58       Expected type: Proxy n0 -> Proxy n0         Actual type: Proxy n -> Proxy n     • In the ambiguity check for ‘foo’       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes       In the type signature:         foo :: forall n. F n => (F n => Proxy n -> Proxy n) -> Int     | 111 | foo :: forall n. F n => (F n => Proxy n -> Proxy n) -> Int     |        ^^^^^^^^^^^^^^^^^^^^ ``` Interestingly adding an equality constraint on `n` does also work: ``` class (KnownNat n, 1 ~ n) => F (n :: Nat) foo :: forall n. F n => (F n => Proxy n -> Proxy n) -> Int foo f = let _ = f (Proxy @n) in 0 ``` Anyone have any clue what is going on here? Best regards, Rowan Goemans