Discrepancy between parsed AST and source code vis-à-vis linear arrows in GADTs
Originally noticed in 7f418acf (comment 304011).
If you define this program:
{-# LANGUAGE GADTs #-}
module Bug where
data T where
MkT :: Int -> T
And compile it with GHC 9.0.1-alpha1 using the -ddump-parsed-ast
flag, you'll get the following output:
({ Bug.hs:1:1 }
(HsModule
(VirtualBraces
(1))
(Just
({ Bug.hs:2:8-10 }
{ModuleName: Bug}))
(Nothing)
[]
[({ Bug.hs:(4,1)-(5,17) }
(TyClD
(NoExtField)
(DataDecl
(NoExtField)
({ Bug.hs:4:6 }
(Unqual
{OccName: T}))
(HsQTvs
(NoExtField)
[])
(Prefix)
(HsDataDefn
(NoExtField)
(DataType)
({ <no location info> }
[])
(Nothing)
(Nothing)
[({ Bug.hs:5:3-17 }
(ConDeclGADT
(NoExtField)
[({ Bug.hs:5:3-5 }
(Unqual
{OccName: MkT}))]
({ Bug.hs:5:10-17 }
(False))
[]
(Nothing)
(PrefixCon
[(HsScaled
(HsLinearArrow)
({ Bug.hs:5:10-12 }
(HsTyVar
(NoExtField)
(NotPromoted)
({ Bug.hs:5:10-12 }
(Unqual
{OccName: Int})))))])
({ Bug.hs:5:17 }
(HsTyVar
(NoExtField)
(NotPromoted)
({ Bug.hs:5:17 }
(Unqual
{OccName: T}))))
(Nothing)))]
({ <no location info> }
[])))))]
(Nothing)
(Nothing)))
In particular, note the use of HsLinearArrow
. The original source code, however, definitely did not use a linear function arrow! This causes problems for exact pretty-printing, which gives @alanz trouble.
Note that the fact that the ->
in MkT :: Int -> T
is interpreted to be linear is itself an expected result. See this part of the linear types proposal, which explains that if the LinearTypes
extension is not enabled, then function arrows in GADT constructor types are always interpreted to be linear. What isn't an expected result is that the AST uses HsLinearArrow
. Generally, we want the AST to match what the user wrote, which isn't happening here.
The culprit is this part of GHC.Parser.PostProcess.mkGadtDecl
:
mkGadtDecl :: [Located RdrName]
-> LHsType GhcPs
-> P (ConDecl GhcPs)
mkGadtDecl names ty = do
linearEnabled <- getBit LinearTypesBit
let (args, res_ty)
| ...
= let (arg_types, res_type) = splitHsFunType body_ty
arg_types' | linearEnabled = arg_types
| otherwise = map (hsLinear . hsScaledThing) arg_types
in (PrefixCon arg_types', res_type)
... }
In the absence of LinearTypes
, the parser always fills in the arguments of a GADT constructor with hsLinear
. Instead of doing this, I propose that the parser (and renamer) leave the HsArrow
s in a GADT constructor type alone. Later in the typechecker, we can then interpret the HsArrow
s based on the presence or absence of LinearTypes
. One possible way to do this would be in GHC.Tc.TyCl.tcConArg
, perhaps like this:
tcConArg :: ContextKind
-> HsScaled GhcRn (LHsType GhcRn) -> TcM (Scaled TcType, HsSrcBang)
tcConArg exp_kind (HsScaled w bty)
= do { traceTc "tcConArg 1" (ppr bty)
; arg_ty <- tcCheckLHsType (getBangType bty) exp_kind
; w' <- tcMult w
-- This is the new part
; linearEnabled <- xoptM LangExt.LinearTypes
; let interp_w
| linearEnabled = w'
| otherwise = oneDataConTy
; traceTc "tcConArg 2" (ppr bty)
; return (Scaled interp_w arg_ty, getBangStrictness bty) }