Type inference fails on polymorphic pair pattern match

[rcook]

Steps to reproduce

Idris version 1.3.1:

$ idris --version
1.3.1

Compile following program:

module Main

import Data.Vect

withFile : String -> (File -> IO (Either FileError a)) -> IO (Either FileError a)
withFile p cb = do
    Right f <- openFile p Read | Left e => pure (Left e)
    result <- cb f
    closeFile f
    pure result

parseLine : String -> List Int
parseLine = map cast . words

toVect : List a -> (n ** Vect n a)
toVect [] = (_ ** [])
toVect (x :: xs) =
    let (_ ** xsVect) = toVect xs
    in (_ ** x :: xsVect)

main : IO ()
main = do
    Right (xs, ys) <- withFile "data.txt" $ \f => do
        Right xLine <- fGetLine f | Left e => pure (Left e)
        Right yLine <- fGetLine f | Left e => pure (Left e)
        pure (Right (parseLine xLine, parseLine yLine))
    | Left e => putStrLn ("FAILED: " ++ show e)

    let (xsLength ** xsVect) = toVect xs
    let (ysLength ** ysVect) = toVect ys

    case exactLength xsLength ysVect of
        Nothing => putStrLn "Vector lengths do not match"
        Just ysVect' => printLn (zipWith (+) xsVect ysVect')

Expected behaviour

I would expect Idris to be able to infer all the types in this program and to be able to successfully compile it.

Observed behaviour

Compilation fails with following error:

Main.idr:23:5-18:
   |
23 |     Right (xs, ys) <- withFile "data.txt" $ \f => do
   |     ~~~~~~~~~~~~~~
When checking left hand side of Main.case block in main at Main.idr:23:23-18:55:
When checking argument r to constructor Prelude.Either.Right:
        Attempting concrete match on polymorphic argument: MkPair xs ys

Follow-up

I can get the program to compile If I fix the type using the as follows:

module Main

import Data.Vect

withFile : String -> (File -> IO (Either FileError a)) -> IO (Either FileError a)
withFile p cb = do
    Right f <- openFile p Read | Left e => pure (Left e)
    result <- cb f
    closeFile f
    pure result

parseLine : String -> List Int
parseLine = map cast . words

toVect : List a -> (n ** Vect n a)
toVect [] = (_ ** [])
toVect (x :: xs) =
    let (_ ** xsVect) = toVect xs
    in (_ ** x :: xsVect)

main : IO ()
main = do
    Right (xs, ys) <- the (IO (Either FileError (List Int, List Int))) $ withFile "data.txt" $ \f => do
        Right xLine <- fGetLine f | Left e => pure (Left e)
        Right yLine <- fGetLine f | Left e => pure (Left e)
        pure (Right (parseLine xLine, parseLine yLine))
    | Left e => putStrLn ("FAILED: " ++ show e)

    let (xsLength ** xsVect) = toVect xs
    let (ysLength ** ysVect) = toVect ys

    case exactLength xsLength ysVect of
        Nothing => putStrLn "Vector lengths do not match"
        Just ysVect' => printLn (zipWith (+) xsVect ysVect')

Perhaps I have overestimated Idris's ability to infer types. If this is the case, I would love to know the explanation for this behaviour. Thanks!

[rcook]

Of course, it's possible to specify a value for the a implicit argument to withFile as in withFile {a = (List Int, List Int)} but this doesn't explain why this cannot be inferred.