Deriving Data turns UNSAFE code to be SAFE
#2432
Comments
kleinreact
changed the title
Data tuns UNSAFE code to be SAFEData turns UNSAFE code to be SAFE
|
My guess is that the code generated by |
|
I've minimized the example module Unsound where
{-@ LIQUID "--save" @-}
import Data.Data
data T = A | B
deriving Data
{-@ toInt :: T -> { i:Nat | false } @-}
toInt :: T -> Int
toInt A = -1
toInt B = undefinedDumped the generated instance But when I manually insert the instance module Unsound where
{-@ LIQUID "--save" @-}
import Data.Data
data T = A | B
instance Data T where
gunfold k z c = case constrIndex c of
1 -> z A
_ -> z B
gfoldl k z A = z A
gfoldl k z B = z B
toConstr A = cA_a18t
toConstr B = cB_a18u
dataTypeOf _ = tT_a18s
{-@ lazy tT_a18s @-}
{-@ lazy cA_a18t @-}
{-@ lazy cB_a18u @-}
tT_a18s :: DataType
cA_a18t :: Constr
cB_a18u :: Constr
tT_a18s = mkDataType "Unsound.T" [cA_a18t, cB_a18u]
cA_a18t = mkConstrTag tT_a18s "A" 1 [] Prefix
cB_a18u = mkConstrTag tT_a18s "B" 2 [] Prefix
{-@ toInt :: T -> { i:Nat | false } @-}
toInt :: T -> Int
toInt A = -1
toInt B = undefinedIt fails the verification so it's some other weird interaction |
|
Ok figured out the issue, the code generated by Instead when the code is manually inserted they don't get a I don't get why LH is putting there a |
|
👋 I see two issues here:
|
|
I think is has something to do with the definitions of Unsound.tT_a18s, Unsound.cA_a18t and Unsound.cB_a18u being non terminating as they are mutually recursive and clearly non terminating, I think that the kvars are set to false when performing termination checking |
The following example is reported to be liquid safe although it isn't. The problem seems to be introduced by the
deriving (Data)clause, as the correct liquid type mismatch gets reported when leaving it out.Tested with 8c550df and GHC 9.10.1.
{-@ LIQUID "" @-} {-# LANGUAGE DeriveDataTypeable #-} {-# OPTIONS_GHC -fplugin=LiquidHaskell #-} module T2432 where import Data.Data (Data) {-@ data T = A | B @-} data T = A | B deriving (Data) {-@ type A = { v : T | v == A } @-} {-@ toInt :: v : A -> { i : Nat | i == 2 } @-} toInt :: T -> Int toInt A = 0 toInt _ = error ""LH reports a cryptic warning at least
The text was updated successfully, but these errors were encountered: