Weird behaviour when passing polytypes to type families
Summary
In the type of a definition, passing polytypes to type families seems to lead to all sorts of weird behaviour.
Steps to reproduce
import Data.Proxy (Proxy)
import Data.Kind (Type)
type family F (b :: Bool) (t1 :: Type) (t2 :: Type) :: Type where
F 'True t1 t2 = t1
F 'False t1 t2 = t2
-- almost works, but gives error when using:
-- f :: forall (a :: Type) (b :: Bool). Proxy a -> Proxy b -> F b (forall (x :: ()). ()) ()
-- f :: forall (a :: Type) (b :: Bool). Proxy a -> Proxy b -> F 'True (forall (x :: a). ()) ()
-- gives nonsense error when checking ambiguity:
f :: forall (a :: Type) (b :: Bool). Proxy a -> Proxy b -> F b (forall (x :: a). ()) ()
f = undefined
The error:
Test.hs:11:6: error:
• Couldn't match type: F b (forall (x :: a). ()) ()
with: F b (forall (x :: a). ()) ()
Expected: Proxy @{Type} a
-> Proxy @{Bool} b -> F b (forall (x :: a). ()) ()
Actual: Proxy @{Type} a
-> Proxy @{Bool} b -> F b (forall (x :: a). ()) ()
NB: ‘F’ is a non-injective type family
• In the ambiguity check for ‘f’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature:
f :: forall (a :: Type) (b :: Bool). Proxy a
-> Proxy b -> F b (forall (x :: a). ()) ()
|
11 | f :: forall (a :: Type) (b :: Bool). Proxy a -> Proxy b -> F b (forall (x :: a). ()) ()
With -XAllowAmbiguousTypes
:
Test.hs:11:6: error:
• Couldn't match type: F b (forall (x :: a). ()) ()
with: F b (forall (x :: a). ()) ()
Expected: Proxy @{Type} a
-> Proxy @{Bool} b -> F b (forall (x :: a). ()) ()
Actual: Proxy @{Type} a
-> Proxy @{Bool} b -> F b (forall (x :: a). ()) ()
NB: ‘F’ is a non-injective type family
• In the ambiguity check for ‘f’
In the type signature:
f :: forall (a :: Type) (b :: Bool). Proxy a
-> Proxy b -> F b (forall (x :: a). ()) ()
|
11 | f :: forall (a :: Type) (b :: Bool). Proxy a -> Proxy b -> F b (forall (x :: a). ()) ()
In the case where it looks like it should work, notably
f :: forall (a :: Type) (b :: Bool). Proxy a -> Proxy b -> F 'True (forall (x :: a). ()) ()
We get the following behaviour:
>>> :t f
f :: forall a (b :: Bool).
Proxy @{Type} a
-> Proxy @{Bool} b -> F 'True (forall (x :: a). ()) ()
>>> :t f (Proxy @Int)
f (Proxy @Int)
:: forall {b :: Bool}. Proxy @{Bool} b -> forall (x :: Int). ()
>>> :t f (Proxy @Int) (Proxy @'True)
f (Proxy @Int) (Proxy @'True) :: forall (x :: Int). ()
>>> f (Proxy @Int) (Proxy @'True)
<interactive>:45:1: error:
• Couldn't match type ‘forall (x1 :: Int). ()’ with ‘()’
Expected: ()
Actual: F 'True (forall (x :: Int). ()) ()
• When checking that the inferred type
it :: F 'True (forall (x :: Int). ()) ()
is as general as its inferred signature
it :: forall (x :: Int). ()
Expected behavior
Either they should work, or give a useful error message. Optimally they would work, since I'm trying to work around returning polytypes from type families.
Environment
- GHC version used: 9.2.3