Unknown func-sort Error

[nikivazou]

The code below crashes with Unknown func-sort error.

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

-- workaround :: List Int -> Int
-- workaround _ = 0

data List a = Nil | Cons a (List a)

{-@ measure llen @-}
llen :: List a -> Int
llen Nil         = 0
llen (Cons _ xs) = 1 + llen xs

{-@ thm :: v:List Double -> { toDouble v <= 1 } @-}
thm ::  List Double -> ()
thm v = ()

{-@ measure toDouble :: a -> Double @-}
{-@ toDouble :: x:a -> {v:Double | v = toDouble x } @-}
toDouble :: a -> Double
toDouble x = undefined

**** LIQUID: ERROR :1:1-1:1: Error
  PANIC: Please file an issue at https://github.com/ucsd-progsys/liquid-fixpoint
Unknown func-sort: (Main.List Int) : Int for (apply : func(0 , [(Main.List @(45));
                   int])) (Main.llen : func(0 , [(Main.List @(45));
                                                 int])) (Main.Nil : (Main.List @(45)))

The problem is that PLE generates a llen Nil term hitting the bugs expected in https://github.com/ucsd-progsys/liquid-fixpoint/blob/develop/src/Language/Fixpoint/Types/Theories.hs#L121-L125

A workaround is to introduce a List Int -> Int function (e.g., by uncommenting the workaround function). A proper fix should add List Int -> Int in the sorts of sortEnv (here: https://github.com/ucsd-progsys/liquid-fixpoint/blob/develop/src/Language/Fixpoint/Solver/Sanitize.hs#L402) This is done for reflected functions but not for measures. (Does fixpoint have access to the measure definitions?)

This should be a new bug, since measures used to be real SMT functions and did not require the apply defunctionalization.

[facundominguez]

I cannot get the reported panic with the latest liquidhaskell. But I get a different panic now:

$ cabal exec ghc -- -package liquidhaskell Test.hs
...

**** LIQUID: ERROR *************************************************************

<no location info>: error:
    Sorry, unexpected panic in liquid-fixpoint!

and liquid-fixpoint says

$ cabal exec fixpoint -- .liquid/Test.hs.bfq --rewriteaxioms


Liquid-Fixpoint Copyright 2013-21 Regents of the University of California.
All Rights Reserved.

Working  66% [============================================.....................]
Crash!: :1:1-1:1: Error
  crash: SMTLIB2 respSat = Error "line 3 column 35747: unknown constant GHC.Err.undefinedReal declared: (declare-fun GHC.Err.undefined () Int) "
CRASH: -1

which is still worth fixing.