Unexpected linear types in pattern matching for pairs

[Junology]

Hello. I found the following simple code doesn't type check with Idris v1.3.0:

test3 : Integer
test3 = let (x,y) = (1,2) in x+y

The error message says about linear types, and it is I think unexpected.

Steps to Reproduce

Main.idr

module Main

test3 : Integer
test3 = let (x,y) = (1,2) in x+y

main : IO ()
main = pure ()

idris Main.idr -o main

Expected Behavior

Compiled successfully.

Observed Behavior

Main.idr:4:13-17:
  |
4 | test3 = let (x,y) = (1,2) in x+y
  |             ~~~~~
Trying to use linear name x in non-linear context

[corazza]

Same here. Idris 1.3.1

Code:

screenScale : Double
screenScale = 33

resolution : (Int, Int)
resolution = (1280, 960)

Cast (Int, Int) (Double, Double) where
  cast (x, y) = (cast x, cast y)

positionToScreen : (camera : Vector2D) -> (position : Vector2D) -> (Int, Int)
positionToScreen (cx, cy) (ox, oy)
  = let (x, y) = screenScale `scale` (ox - cx, oy - cy)
        (asdf1, asdf2) = the (Double, Double) (cast resolution) in -- ERROR HERE
            cast (x - asdf1/2, y - asdf2/2)

Error message: Trying to use linear name asdf1 in non-linear context