Skip to content

Template Haskell gets confused around visible dependent quantification

If I say

$( do ty <- [d| {-# SPECIALISE id :: forall a -> a -> a #-} |]
      runIO $ print ty
      return [] )

I see

[PragmaD (SpecialiseP GHC.Base.id (ForallT [PlainTV a_6989586621679025225] [] (AppT (AppT ArrowT (VarT a_6989586621679025225)) (VarT a_6989586621679025225))) Nothing AllPhases)]

Note that the output has a normal ForallT, not a ForallVisT.

This is because splitLHsForAllTy is used (within splitLHsSigmaTy). I conjecture that most uses of splitLHsForAllTy are wrong. Instead, callers should use splitLHsForAllTyInvis, which distinguishes between visible and invisible dependent quantification. Indeed, perhaps splitLHsForAllTy should be deleted, entirely.

Tagging @RyanGlScott, who knows both about VDQ and TH, happily.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information