[Haskellcafe] Typechecker complains about untouchable types
rowan goemans
goemansrowan at gmail.com
Wed Apr 6 19:29:20 UTC 2022
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:858
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:858
‘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:858
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
More information about the HaskellCafe
mailing list