Skip to content

Assertion failure with typed Template Haskell type variable

File:

{-# LANGUAGE TemplateHaskell, RankNTypes #-}
module M where
import Language.Haskell.TH.Syntax

data T = MkT (forall a. a)
f x = [|| MkT $$(x) ||]

In 9.2 and earlier, this compiles, even with -dcore-lint enabled. But the inferred type, f :: Q (TExp a) -> Q (TExp T), is wrong; that'd be correct if MkT :: a -> T while MkT :: (forall a. a) -> T.

In master, this gives an assertion failure about levels inside writeMetaTyVarRef. If assertions are disabled, it fails Lint.

*** Core Lint errors : in result of Desugar (before optimization) ***
M.hs:6:1: warning:
    The type variable @a_a1W4[sk:2] is out of scope
    In the type of a binder: f
    In the type ‘forall {m :: * -> *}.
                 Quote m =>
                 Code m a_a1W4[sk:2] -> Code m T’
    Substitution: [TCvSubst
                     In scope: InScope {m_a1Ib}
                     Type env: [a1Ib :-> m_a1Ib]
                     Co env: []]

This looks related to #19893, but I'm not sure if it's the same bug.

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