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