GHC does not honor unrestricted function types for GADTs in TH splices

The linear types proposal says this about arrow types in GADT constructors:

With the GADT syntax, multiplicity of the arrows is honoured:

data Foo2 where
  Bar2 :: A #-> B -> Foo2

means that Bar2 :: A #-> B -> Foo2. [...] This only holds in modules with -XLinearTypes turned on

However, this claim is not true in practice. Here is a counterexample:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE TemplateHaskell #-}
module Bug where

import Data.Foldable
import Language.Haskell.TH

data T1 where
  MkT1 :: Int #-> Int -> T1

$([d| data T2 where
        MkT2 :: Int #-> Int -> T2
    |])

$(pure [])

main :: IO ()
main = do
  putStrLn $(reify 'MkT1 >>= stringE . pprint)
  putStrLn $(reify 'MkT2 >>= stringE . pprint)

This program will declare two GADTs whose constructors have the same types (modulo GADT return types) and then print out their types. Surprisingly, this program reports different types for MkT1 and MkT2:

λ> main
Constructor from Bug.T1: Bug.MkT1 :: GHC.Types.Int #->
                                     GHC.Types.Int -> Bug.T1
Constructor from Bug.T2: Bug.MkT2 :: GHC.Types.Int #->
                                     GHC.Types.Int #-> Bug.T2

This reports that the type of MkT1 is Int #-> Int -> T1 while the type of MkT2 is Int #-> Int #-> T2. In particular, the second arrow type in MkT2 is linear, which is not what I declared it to be!

cc @monoidal