Newtypes are unrolled when using embed

[clayrat]

Currently, if we want to embed a specialization of some type in a LF theory, both type and newtype definitions get unrolled, breaking the abstraction barrier. E.g., defining bags as follows:

import qualified Data.Map      as M

{-@ embed   Bag as Bag_t @-}
{-@ measure Bag_empty :: Int -> Bag a @-}
{-@ measure Bag_count :: Bag a -> a -> Int @-}

newtype Bag a = Bag { toMap :: M.Map a Int }

{-@ assume empty :: {v:Bag k | v = Bag_empty 0} @-}
empty :: Bag k
empty = Bag M.empty

{-@ assume get :: (Ord k) => k:k -> b:Bag k -> {v:Nat | v = Bag_count b k}  @-}
get :: (Ord k) => k -> Bag k -> Int
get k b = M.findWithDefault 0 k (toMap b)

generates an .fq file where empty and get internally reference Data.Map symbols, which causes trouble down the line when we want to interop with SMT Bag theory. To maintain the Bag_t abstraction, we must define Bags as data Bag a = Bag { toMap :: M.Map a Int }. This gives us proper theory definitions at the cost of runtime performance, as single-constructor data definitions are not optimized away in the same way as newtypes. Intuitively, we should probably only unroll type definitions, and treat newtype ones equally to data.

[nikivazou]

If I remember correctly, this happens from GHC. LH does not see the newtypes.

[facundominguez]

It would be possible to transform the source code before feeding it to the desugarer, and change the newtypes to data. This could break code that uses Data.Coerce.coerce, but perhaps we don't have to deal with that if the transformation is done after typechecking.

[facundominguez]

which causes trouble down the line when we want to interop with SMT Bag theory.

Which trouble is caused exactly? The specs would still refer to Bag. Perhaps LH is finding type mismatches? If so these tests could be relaxed to make newtypes compatible with their representations.

[clayrat]

The trouble is that all the generated constants and binds reference Data.Map.Internal.Map @(0) int (i.e., the underlying implementation) instead of Bag_t @(0) which then causes the LF elaborator to crash whenever you try actually to use the type :) E.g. this is what gets generated from a newtype definition (and crashes):

constant Language.Haskell.Liquid.Bag.Bag : (func(1 , [(Data.Map.Internal.Map @(0) int);
                                                      (Data.Map.Internal.Map @(0) int)]))
constant Language.Haskell.Liquid.Bag.empty : (func(1 , [(Data.Map.Internal.Map @(0) int)]))
constant Language.Haskell.Liquid.Bag.get : (func(1 , [@(0);
                                                      (Data.Map.Internal.Map @(0) int);
                                                      int]))
constant Language.Haskell.Liquid.Bag.put : (func(1 , [@(0);
                                                      (Data.Map.Internal.Map @(0) int);
                                                      (Data.Map.Internal.Map @(0) int)]))
constant Language.Haskell.Liquid.Bag.toMap : (func(1 , [(Data.Map.Internal.Map @(0) int);
                                                        (Data.Map.Internal.Map @(0) int)]))

and this is the data definition that works as intended:

constant Language.Haskell.Liquid.Bag.Bag : (func(1 , [(Data.Map.Internal.Map @(0) int);
                                                      (Bag_t @(0))]))
constant Language.Haskell.Liquid.Bag.empty : (func(1 , [(Bag_t @(0))]))
constant Language.Haskell.Liquid.Bag.get : (func(1 , [@(0);
                                                      (Bag_t @(0));
                                                      int]))
constant Language.Haskell.Liquid.Bag.put : (func(1 , [@(0);
                                                      (Bag_t @(0));
                                                      (Bag_t @(0))]))
constant Language.Haskell.Liquid.Bag.toMap : (func(1 , [(Bag_t @(0));
                                                        (Data.Map.Internal.Map @(0) int)]))

[facundominguez]

I see. Despite the fact that GHC erases newtypes, it looks like it should be possible to generate those constants with the Bag occurrences found in the specs.

I'm not sure about the binds. I expect a few binds to be generated (beyond what the user wrote herself), and LH would need to correctly infer Bag sorts for them.