LiquidHaskell: Tracing Data

Continuing where I left off last time, I decided to figure out how to print a few variables to check how data is parsed and transformed.

The types I was most interested in printing were LogicMap, LogicNameEnv, and Spec LocSymbol BareTypeParsed (the type of sp2).

LogicMap and Spec LocSymbol BareTypeParsed were very straightforward as they are both instances of the PPrint class, which provides many convenient functions to show data in a human readable format.

LogicNameEnv required manually accessing its fields and transforming each into an equivalent LHName which could then be printed.

The printing itself is just calling trace, from the Debug.Trace module.

Running a test

I ran LH on this very simple piece of code:

{-@ LIQUID "--typeclass" @-}
module Basic where

import Prelude (Bool (True), (==))

class Eq a where
    {-@ eq :: a -> a -> Bool @-}
    eq :: a -> a -> Bool

class Eq a => VEq a where
    {-@ lawRefl :: v:a -> {eq v v == True} @-}
    lawRefl :: a -> ()

And these are the results I got:

==> sp2:
dataDecls = []
classes = []
sigs =
  [ eq : lq_tmp$db##0:a -> lq_tmp$db##1:a -> GHC.Internal.Types.Bool
  , lawRefl : v:a -> {VV : _ | eq v v == True}
  ]

==> lmap1:
Logic Map
  logic-map
    GHC.Internal.Base.$ := $[f, x]|->f x
    GHC.Internal.Bignum.Integer.IS := IS[x]|->x
    GHC.Internal.CString.unpackCString# := unpackCString#[x]|->x
    GHC.Internal.Classes.not := not[x]|->not x
    GHC.Internal.Num.abs := abs[x]|->if x >= 0 then x else -x
    GHC.Internal.Real.div := div[x, y]|->x / y
    GHC.Internal.Real.fromIntegral := fromIntegral[x]|->x
    GHC.Internal.Real.mod := mod[x, y]|->x mod y
    GHC.Internal.Real.quot := quot[x, y]|->if x >= 0 then (if y >= 0 then x / y else -x / (-y)) else -(-x) / y
    GHC.Internal.Real.rem := rem[x, y]|->if x >= 0 then (if y >= 0 then x mod y else x mod (-y)) else -(-x) mod y
    GHC.Internal.Types.True := True[]|->true
    cons := cons[x, xs]|->GHC.Internal.Types.: x xs
    nil := nil[]|->GHC.Internal.Types.[]
  axiom-map

==> logicNameEnv0:
lneLHName entries:
  "GHC.Base_LHAssumptions.comp" -> GHC.Base_LHAssumptions.comp
  "GHC.Internal.Real.div" -> GHC.Internal.Real.div
  "GHC.Internal.Real.rem" -> GHC.Internal.Real.rem
  "mod" -> mod
  "rem" -> rem
  "GHC.Internal.Base.." -> GHC.Internal.Base..
  "Data.Tuple_LHAssumptions.fst" -> fst
  "GHC.Internal.Real.quot" -> GHC.Internal.Real.quot
  "fromIntegral" -> fromIntegral
  "GHC.Internal.Num.abs" -> GHC.Internal.Num.abs
  "$" -> $
  "GHC.Internal.CString.unpackCString#" -> GHC.Internal.CString.unpackCString#
  "GHC.Maybe_LHAssumptions.lq_tmp$db##0" -> lq_tmp$db##0
  "GHC.Internal.Base.$" -> GHC.Internal.Base.$
  "div" -> div
  "GHC.Internal.Bignum.Integer.IS" -> GHC.Internal.Bignum.Integer.IS
  "Prelude_LHAssumptions.Min" -> Min
  "nil" -> nil
  "quot" -> quot
  "GHC.Internal.Classes.not" -> GHC.Internal.Classes.not
  "cons" -> cons
  "GHC.Types_LHAssumptions.len" -> len
  "GHC.Internal.Types.True" -> GHC.Internal.Types.True
  "not" -> not
  "Liquid.Prelude.Totality_LHAssumptions.totalityError" -> totalityError
  "Prelude_LHAssumptions.Max" -> Max
  "Data.Tuple_LHAssumptions.snd" -> snd
  "True" -> True
  "GHC.Base_LHAssumptions.autolen" -> autolen
  "GHC.Types_LHAssumptions.addrLen" -> addrLen
  "abs" -> abs
  "GHC.Internal.Real.mod" -> GHC.Internal.Real.mod
  "unpackCString#" -> unpackCString#
  "IS" -> IS
  "GHC.Internal.Real.fromIntegral" -> GHC.Internal.Real.fromIntegral

Reflected entries:
  comp -> GHC.Base_LHAssumptions.comp
  . -> GHC.Internal.Base..

And just for completeness sake, this is the error I get:

typeclasses/pos/Basic.hs:11:28: error:
    Unknown logic name `eq`
    Cannot resolve name
    Maybe you meant one of: len
   |
11 |     {-@ lawRefl :: v:a -> {eq v v == True} @-}
   |                            ^^

However, from the logs being generated in the Plugin.hs file, we have:

mg_exports => [VEq{VEq, lawRefl}, Eq{Eq, eq}]
mg_tcs => [VEq, Eq]

So typeclasses are being parsed, it’s just that they are not visible to the name resolver. That doesn’t mean the solution is straightforward, as I’m still not sure when and how exactly to make typeclasses methods available to the resolver. But, I believe this has been step forward in the right direction.