GitLab

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 HsArrows in a GADT constructor type alone. Later in the typechecker, we can then interpret the HsArrows 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) }