Elaboration fails due to `return`

[ranjitjhala]

This simple code

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

module Elab where

main :: IO ()
main = return ()

{-@ incr :: x:Int -> {v:Int | v > x} @-}
incr :: Int -> Int
incr x = x + 1

fails with the rather horrific error

**** LIQUID: ERROR :1:1-1:1: Error
  elaborate solver elabBE 89 "Elab.main" {VV##427 : func(0 , [(GHC.Prim.State# GHC.Prim.RealWorld);
                     (Tuple (GHC.Types.TupleRep (GHC.Types.$91$$93$ GHC.Types.RuntimeRep)) GHC.Types.LiftedRep (GHC.Prim.State# GHC.Prim.RealWorld) Tuple)]) | [(VV##427 = (GHC.Base.return GHC.Tuple.$40$$41$))]} failed on:
      VV##427 == GHC.Base.return GHC.Tuple.()
  with error
      Cannot unify func(0 , [(GHC.Prim.State# GHC.Prim.RealWorld);
          (Tuple (GHC.Types.TupleRep (GHC.Types.$91$$93$ GHC.Types.RuntimeRep)) GHC.Types.LiftedRep (GHC.Prim.State# GHC.Prim.RealWorld) Tuple)]) with (@(43) Tuple) in expression: VV##427 == GHC.Base.return GHC.Tuple.()
  because
Elaborate fails on VV##427 == GHC.Base.return GHC.Tuple.()
  in environment
      GHC.Base.return := func(2 , [@(0); (@(1) @(0))])

      GHC.Tuple.() := Tuple

      VV##427 := func(0 , [(GHC.Prim.State# GHC.Prim.RealWorld);
                           (Tuple (GHC.Types.TupleRep (GHC.Types.$91$$93$ GHC.Types.RuntimeRep)) GHC.Types.LiftedRep (GHC.Prim.State# GHC.Prim.RealWorld) Tuple)])

I am surprised that there is a refinement somewhere with return () inside it.

I believe this has to do with the makeSingleton and the fact that it makes singleton types for function-applications -- clearly its (a) doing the wrong thing here? or (b) should not be used here and the higherOrder flag should only be applied to functions who are being reflected and not everywhere?

-- | create singleton types for function application
makeSingleton :: CGEnv -> CoreExpr -> SpecType -> SpecType
makeSingleton γ e t
  | higherOrderFlag γ, App f x <- simplify e
  = case (funExpr γ f, argForAllExpr x) of
      (Just f', Just x')
                 | not (GM.isPredExpr x) -- (isClassPred $ exprType x)
                 -> strengthenMeet t (uTop $ F.exprReft (F.EApp f' x'))
      (Just f', Just _)
                 -> strengthenMeet t (uTop $ F.exprReft f')
      _ -> t
  | rankNTypes (getConfig γ)
  = case argExpr γ (simplify e) of
       Just e' -> strengthenMeet t $ (uTop $ F.exprReft e')
       _       -> t
  | otherwise
  = t
  where
    argForAllExpr (Var x)
      | rankNTypes (getConfig γ)
      , Just e <- M.lookup x (forallcb γ)
      = Just e
    argForAllExpr e
      = argExpr γ e

^^ @nikivazou do you know what the above code is for? Why do we do all this extra stuff for function applications in makeSingleton?

[nikivazou]

The problem seems to be that the type parameter of return is not properly instantiated, no?

I do not recall exactly why we need all these stuff in makeSingleton. Did you try removing them and see what fails?

[facundominguez]

I cannot reproduce in the latest LH.