[Haskell-cafe] Typechecker complains about untouchable types

[rowan goemans]

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