Summary

The desugaring of FFI-defined functions drops linearity information.

Steps to reproduce

The following module

{-# 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 ***

Expected behavior

Linear FFI functions are perfectly reasonable a thing to have. So we should desugar them properly. This was actually spotted in review: !852 (diffs) . It's a matter of pushing the information until this spot.

Environment

• GHC version used: current master