FFI and linear types

[monoidal]

FFI currently does not behave well with linear types: https://gitlab.haskell.org/ghc/ghc/-/merge_requests/852/diffs?diff_id=9699#cf5b233b6ec5c0a6951d1018fee507d2d2d71391_274_274

The goal is to decide whether we allow linear types there and check the code.

[aspiwack]

@monoidal Can we make an example of this misbehaving?

[monoidal]

{-# LANGUAGE LinearTypes #-}
module II where

foreign import ccall "exp" c_exp :: Double #-> Double

fails linear lint:

*** Core Lint errors : in result of Desugar (before optimization) ***
II.hs:4:1: warning:
    Linearity failure in lambda: ds_du1
    'Many ⊈ 'One
    In the RHS of c_exp :: Double #-> Double
    In the body of lambda with binder ds_du1 :: Double
    Substitution: [TCvSubst
                     In scope: InScope {}
                     Type env: []
                     Co env: []]
II.hs:4:1: warning:
    Linearity failure in lambda: ds_du1
    'Many ⊈ 'One
    In the RHS of c_exp :: Double #-> Double
    In the unfolding of c_exp :: Double #-> Double
    In the body of lambda with binder ds_du1 :: Double
    Substitution: [TCvSubst
                     In scope: InScope {}
                     Type env: []
                     Co env: []]
*** Offending Program ***
Rec {
$wccall_du7
  :: Double# -> State# RealWorld -> (# State# RealWorld, Double# #)
[LclId]
$wccall_du7
  = \ (ds_du3 :: Double#) ->
      {__pkg_ccall_GC main Double#
                     -> State# RealWorld -> (# State# RealWorld, Double# #)}_du6
        ds_du3

c_exp :: Double #-> Double
[LclIdX,
 Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True,
         Guidance=ALWAYS_IF(arity=1,unsat_ok=False,boring_ok=False)
         Tmpl= \ (ds_du1 [Occ=Once!] :: Double) ->
                 case ds_du1 of { D# ds_du3 [Occ=Once] ->
                 case $wccall_du7 ds_du3 realWorld# of
                 { (# _ [Occ=Dead], ds_du4 [Occ=Once] #) ->
                 D# ds_du4
                 }
                 }}]
c_exp
  = (\ (ds_du1 :: Double) ->
       case ds_du1 of ds_du2 { D# ds_du3 ->
       case $wccall_du7 ds_du3 realWorld# of wild_00
       { (# ds_du5, ds_du4 #) ->
       D# ds_du4
       }
       })
    `cast` (<Double #-> Double>_R
            :: (Double #-> Double) ~R# (Double #-> Double))

$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "II"#)
end Rec }

*** End of Offense ***

My instinct would be to forbid linearity in FFI for now. Maybe later.

[aspiwack]

Moved to upstream:#18472.