"elaborate solver" crash deriving a generic instance

[plredmond]

Repro code

Repro7.hs

{-# 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 *************************************************************

<no location info>: 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]

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]

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]

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

[plredmond]

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]

@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]

Ugh sorry about that. Probably best to

1. Keep those instances in a separate file
2. 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: @.***>