PLE generates polymorphic applys for Sets

[clayrat]

The combination of the following two files crashes LH:

Foo.hs

{-@ LIQUID "--reflection"     @-}

module Foo where

import Prelude hiding (last)

{-@ reflect last @-}
{-@ last :: xs:{ [a] | len xs > 0 } -> a @-}
last :: [a] -> a
last [x]      = x
last (_ : xs) = last xs

data Foo t = Foo1 -- | Foo2
  deriving (Eq, Ord)

{-@ reflect isFoo @-}
isFoo :: Foo t -> Bool
isFoo Foo1 = True
-- isFoo Foo2 = False

{-@ reflect foos @-}
{-@ foos :: Foo t -> [{ v:Foo t | isFoo v }] @-}
foos :: Foo t -> [Foo t]
foos f = if isFoo f then f : [] else []

Bar.hs

{-@ LIQUID "--reflection"     @-}
{-@ LIQUID "--ple"            @-}

module Bar where

import Prelude hiding (last)
import Data.Set
import Foo

{-@ lemma_last_isFoo :: f : Foo t -> { isFoo (last (foos f))} @-}
lemma_last_isFoo :: Foo t -> ()
lemma_last_isFoo f = if isFoo f then () else ()

The (prettifed) error is :

Unknown func-sort:
 Int : (Array (Foo Int) Bool) for

(apply    : func(0 , [[(Foo t)]; (Array_t (Foo t) bool)]))
(listElts : func(0 , [[(Foo t)]; (Array_t (Foo t) bool)]))
((apply : func(0 , [[(Foo t)]; [(Foo t)]]))
  ((apply : func(0 , [(Foo t); [(Foo t)]; [(Foo t)]]))
   (GHC.Types.: : func(0 , [(Foo t); [(Foo t)]; [(Foo t)]]))
   ((f : (Foo t)) : (Foo t)) : func(0 , [[(Foo t)];
    [(Foo t)]]))
  (GHC.Types.[] : [(Foo t)]) : [(Foo t)])

The bug crucially depends on having 2 files and importing Data.Set, merging the files or removing the import makes it disappear.

[clayrat]

This seems related to the following function and its description: https://github.com/ucsd-progsys/liquid-fixpoint/blob/develop/src/Language/Fixpoint/Types/Theories.hs#L116-L143