"elaborate solver" crash deriving a generic instance

plredmond commented 2 years ago

Repro code

Repro7.hs

```haskell {-# LANGUAGE DeriveGeneric #-} module Repro7 where import GHC.Generics (Generic) {-@ data D = D { x::Nat, y::() } @-} data D = D { x::Int, y::() } deriving Generic ```

Expected behavior

LH does not crash.
LH does not say "unsafe" about contents of a derived Generic instance.

Actual behavior

"elaborate solver" crash

``` [22 of 23] Compiling Repro7 **** LIQUID: ERROR ************************************************************* : error: /Users/mote/code/cbcast-lh:1:1-1:1: Error elaborate solver elabBE 110 "lq_anf$##7205759403792807382##d3Ai" {lq_tmp$x##604 : (GHC.Generics.$58$$42$$58$ (GHC.Prim.TYPE GHC.Types.LiftedRep) int Tuple x##a2VS) | [(lq_tmp$x##604 = lq_anf$##7205759403792807381##d3Ah); (lq_tmp$x##604 = (GHC.Generics.$58$$42$$58$ ds_d3Aa ds_d3Ab)); (lq_tmp$x##604 ~~ (coerce (GHC.Generics.$58$$42$$58$ (GHC.Prim.TYPE GHC.Types.LiftedRep) int Tuple x##a2VS) ~ (GHC.Generics.$58$$42$$58$ GHC.Types.Type int Tuple x##a2VS) in lq_anf$##7205759403792807380##d3Ag))]} failed on: lq_tmp$x##604 == lq_anf$##7205759403792807381##d3Ah && lq_tmp$x##604 == GHC.Generics.:*: ds_d3Aa ds_d3Ab && lq_tmp$x##604 ~~ (coerce (GHC.Generics.$58$$42$$58$ (GHC.Prim.TYPE GHC.Types.LiftedRep) int Tuple x##a2VS) ~ (GHC.Generics.$58$$42$$58$ GHC.Types.Type int Tuple x##a2VS) in lq_anf$##7205759403792807380##d3Ag) with error The sort (@(468) @(470)) is not numeric because Cannot unify (@(468) @(470)) with int in expression: GHC.Generics.:*: ds_d3Aa in environment GHC.Generics.:*: := func(4 , [(@(1) @(3)); (@(2) @(3)); (GHC.Generics.$58$$42$$58$ @(0) @(1) @(2) @(3))]) ds_d3Aa := int ds_d3Ab := Tuple lq_anf$##7205759403792807380##d3Ag := (GHC.Generics.$58$$42$$58$ (GHC.Prim.TYPE GHC.Types.LiftedRep) int Tuple x##a2VS) lq_anf$##7205759403792807381##d3Ah := (GHC.Generics.$58$$42$$58$ (GHC.Prim.TYPE GHC.Types.LiftedRep) int Tuple x##a2VS) lq_tmp$x##604 := (GHC.Generics.$58$$42$$58$ (GHC.Prim.TYPE GHC.Types.LiftedRep) int Tuple x##a2VS) ```

Removing either field fixes.
Changing Nat to Int in refinement fixes.
Changing Nat to {z:Int | z < 0} does not fix (so it seems any refinement causes the problem).
Changing () to another type such as Bool does not fix (so it seems the issue is related to having multiple fields, possibly something to do with the :*: constructor in GHC.Generics).

Versions affected

AFFECTED: (jun 2022) liquidhaskell@https://github.com/ucsd-progsys/liquidhaskell/commit/316c964b5b4f62c9dd96c6b037134fcf3c47f3e4, https://github.com/ucsd-progsys/liquid-fixpoint/commit/7e18f70ede589c5f7f2e0b5a3bf38250938aee28
NOT AFFECTED: (may 2022) liquidhaskell@https://github.com/ucsd-progsys/liquidhaskell/commit/fdbf4f67b, https://github.com/ucsd-progsys/liquid-fixpoint/commit/08fa6b6

facundominguez commented 2 years ago

Thanks @plredmond. Probably a dive into the elaboration code is worth to understand and fix this failure.

One side question is whether LH should be in the business of analyzing these automatically derived instances.

ranjitjhala commented 2 years ago

It shouldn't and I thought there was already a flag to skip doing that?

On Wed, Jun 29, 2022 at 5:18 AM Facundo Domínguez @.***> wrote:

Thanks @plredmond https://urldefense.com/v3/__https://github.com/plredmond__;!!Mih3wA!G4XWnHS_YRzugZgHwbmJkvjt1jWbaNQO_MVlzyS_1PqnDVdJOHGwhjCfk-67U3r1KV4zhDTB-2s_q3r22vhnZvtr$. Probably a dive into the elaboration code is worth to understand and fix this failure.

One side question is whether LH should be in the business of analyzing these automatically derived instances.

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/2019*issuecomment-1169910022__;Iw!!Mih3wA!G4XWnHS_YRzugZgHwbmJkvjt1jWbaNQO_MVlzyS_1PqnDVdJOHGwhjCfk-67U3r1KV4zhDTB-2s_q3r22nAfrYj4$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OEFVS3MTIQBCMBD2J3VRQ5H7ANCNFSM52EO4L7Q__;!!Mih3wA!G4XWnHS_YRzugZgHwbmJkvjt1jWbaNQO_MVlzyS_1PqnDVdJOHGwhjCfk-67U3r1KV4zhDTB-2s_q3r22vSvJGaB$ . You are receiving this because you are subscribed to this thread.Message ID: @.***>

ranjitjhala commented 2 years ago

@plredmond does this work with --no-class-check ?

plredmond commented 2 years ago

I tried adding {-@ LIQUID "--no-class-check" @-} to the file, but it did not resolve the issue.

[Edit: {-@ LIQUID "--skip-module" @-} resolves it, but that has other implications.]

plredmond commented 2 years ago

@lkuper hit this bug today because the tip of one of our development branches derives generic instances of data structures for serialization (https://github.com/lsd-ucsc/cbcast-lh/blob/964f6452612e8d4045210cd40f18af5d0a52dba9/lib/CBCAST.hs#L57-L59)

ranjitjhala commented 2 years ago

Ugh sorry about that. Probably best to

Keep those instances in a separate file
Do compile-spec to NOT run LH on those files

(Till this is fixed)

On Thu, Jul 14, 2022 at 3:23 PM plredmond @.***> wrote:

@lkuper https://urldefense.com/v3/__https://github.com/lkuper__;!!Mih3wA!B6SKyShQVCiocfzqYfS8EB0GpZgWQ4__QnbNEUVGlAJkBB2ydUB-vuQw5Q9SuP08rPqzn2O9B9tFfxvC-rHWdzY4$ hit this bug today because the tip of one of our development branches derives generic instances of data structures for serialization ( https://github.com/lsd-ucsc/cbcast-lh/blob/964f6452612e8d4045210cd40f18af5d0a52dba9/lib/CBCAST.hs#L57-L59 https://urldefense.com/v3/__https://github.com/lsd-ucsc/cbcast-lh/blob/964f6452612e8d4045210cd40f18af5d0a52dba9/lib/CBCAST.hs*L57-L59__;Iw!!Mih3wA!B6SKyShQVCiocfzqYfS8EB0GpZgWQ4__QnbNEUVGlAJkBB2ydUB-vuQw5Q9SuP08rPqzn2O9B9tFfxvC-ohKS_q2$ )

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/2019*issuecomment-1184952335__;Iw!!Mih3wA!B6SKyShQVCiocfzqYfS8EB0GpZgWQ4__QnbNEUVGlAJkBB2ydUB-vuQw5Q9SuP08rPqzn2O9B9tFfxvC-nTlaKjk$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OEIOFOQ6KYVN2VB3EDVUCHOFANCNFSM52EO4L7Q__;!!Mih3wA!B6SKyShQVCiocfzqYfS8EB0GpZgWQ4__QnbNEUVGlAJkBB2ydUB-vuQw5Q9SuP08rPqzn2O9B9tFfxvC-klq0NLv$ . You are receiving this because you commented.Message ID: @.***>

ucsd-progsys / liquidhaskell