Template Haskell + hs-boot = Not in scope during type checking, but it passed the renamer

I don't think this is a very harmful bug but it definitely is a bug. Consider:

-- A.hs-boot
module A where
data T

-- B.hs
module B (module A) where
import {-# SOURCE #-} A

-- A.hs
{-# LANGUAGE TemplateHaskell #-}
module A where
import qualified B
import Language.Haskell.TH
f :: B.T -> B.T
f x = x
$( return [] )
data T = T B.T

The point of the splice is to convince GHC to typecheck f :: B.T -> B.T before it typechecks the type declaration. But this is not going to work, because tcLookupGlobal is going to bail if (1) T is not in the tcg_type_env and (2) T comes from this module.

It would be a simple matter to improve the error message but from a user's perspective, there is no good reason for this to not typecheck. On the implementation side, I am sympathetic to not letting this typecheck: if it does typecheck, then some TyCons will incorrectly refer to the definition from the hs-boot file, rather than our local definition.

Trac metadata

Trac field	Value
Version	8.0.1-rc2
Type	Bug
TypeOfFailure	OtherFailure
Priority	low
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 3

added Tbug Trac import backpack typechecker labels

mentioned in issue #12035 (closed)

Trac metadata

Trac field	Value
Component	Compiler (Type checker) → Template Haskell

added hs-boot label

mentioned in issue #12063

Here is a restriction for hs-boot files and TH which might solve this problem: all TYPEs in the hs-boot file (values can wait) must be defined in the section of the file PRIOR to the first Template Haskell splice. This ensures we have a consistent environment for knot-tying, and also is an obvious place to check for missing types #12063 or type synonym loops #12042 (closed).

Or alternatively re-typecheck the interface produced from the bit before the splice, just as we would do if the bit before the splice was in another module.

How do would you suggest we actually do the retypechecking? For example, in GhcMake we can retypecheck because we're responsible for managing the HPT; but the retypecheck would have to work within the typechecker code.

I have a situation with a {{{makeClassy}} classy lens class cycle that I cannot break (modulo manually expanding the TH). I'd like something like an intra-module hs-boot file to fix this.

I gather from this issue that I shouldn't waste time breaking up my module, as .hs-boot as it currently stands won't save me.

Replying to [ticket:12034#comment:120211 ezyang]:

Here is a restriction for hs-boot files and TH which might solve this problem....

Ezyang's proposal would also not help because the splice defines the Has* class.

I believe the staging restriction as it currently stands ought just to apply to code executed as part of a TH splice. Quoted variable resolution should be fine: if and only the user uses one of the APIs to learn more about a defintion, they should only hit a Nothing/exception because a staging restriction.

intra-module hs-boot would then be a way to assert that some further-down splice defines some names, enough for names, including quoted names, to resolve.

added Plow label