Partial type signature solution "too rigid" when using required type arguments
{-# LANGUAGE RequiredTypeArguments, PartialTypeSignatures, DataKinds #-}
import GHC.TypeLits
data Foo (n :: Nat) = MkFoo
mkFoo :: forall n -> Foo n
mkFoo n = MkFoo
blah :: forall (n :: Nat) -> _
blah n = mkFoo n
Here, instead of inferring w ~ Foo n
, GHC 9.12.1 fails with:
/tmp/b.hs:11:10: error: [GHC-25897] • Couldn't match expected type ‘w’ with actual type ‘Foo n’ ‘w’ is a rigid type variable bound by the inferred type of blah :: forall (n1 :: Nat) -> w at /tmp/b.hs:11:1-16 • In the expression: mkFoo n In an equation for ‘blah’: blah n = mkFoo n • Relevant bindings include blah :: forall (n :: Nat) -> w (bound at /tmp/b.hs:11:1) | 11 | blah n = mkFoo n | ^^^^^^^
If I don't use a required type argument in the definition of blah
, it goes through:
{-# LANGUAGE ScopedTypeVariables #-}
blah :: forall n. _
blah = MkFoo @n
and it gives the correct wildcard filling:
• Found type wildcard ‘_’ standing for ‘Foo n’ Where: ‘n’ is a rigid type variable bound by the inferred type of blah :: Foo n at /tmp/b.hs:18:16 • In the type signature: blah :: forall n. _
Edited by sheaf