Skip to content

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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information