Nested data types are not encoded well

nikivazou commented 5 years ago

e.g.,

{-@ LIQUID "--exactdc"  @-}

data Pred l 
  = PTerm l

data Term l 
  = TPred (Pred (Term l))
  | TTerm  

{-@ measure tsize @-}
tsize :: Term l -> Int
{-@ tsize :: Term l -> Nat @-}
tsize (TPred _)            = 0

crashed with the following elaboration error:

Elaborate fails on Main.TPred##lqdc##$select##Main.TPred##1 lq_tmp$x##594 == ds_dY4
  in environment
      Main.TPred := func(1 , [(Main.Pred Main.Term); (Main.Term @(0))])

      Main.TPred##lqdc##$select##Main.TPred##1 := func(1 , [(Main.Term @(0));
                                                            (Main.Pred Main.Term)])

      Main.tsize := func(1 , [(Main.Term @(0)); int])

      ds_dXY := (Main.Term l##aWM)

      ds_dY4 := (Main.Pred (Main.Term l##aWM))

      is$Main.TPred := func(1 , [(Main.Term @(0)); bool])

      is$Main.TTerm := func(1 , [(Main.Term @(0)); bool])

      lq_tmp$x##594 := (Main.Term l##aWM)

The type of the predicate selector is wrong since the type variable is removed.

nikivazou commented 5 years ago

Worse: after the fix for #1365 the error is

:1:1-1:1: Error
  crash: SMTLIB2 respSat = Error "line 30 column 200: unknown sort 'Main.Term'"

ranjitjhala commented 5 years ago

I really don’t think types like this can be encoded using SMTLIB ... (we can ask/confirm with the experts ...) imo the solution is to just use the old LH encoding for types like these.

nikivazou commented 5 years ago

They can, but we need to use the new encoding.... https://github.com/Z3Prover/z3/issues/1903#issuecomment-433569496

On Fri, Oct 26, 2018, 11:07 PM Ranjit Jhala notifications@github.com wrote:

I really don’t think types like this can be encoded using SMTLIB ... (we can ask/confirm with the experts ...) imo the solution is to just use the old LH encoding for types like these.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1366#issuecomment-433585910, or mute the thread https://github.com/notifications/unsubscribe-auth/AArotaK4G_QvJOTY0ypebo0NhK97J659ks5uo83fgaJpZM4X9BXo .

ucsd-progsys / liquidhaskell

Nested data types are not encoded well #1366