Abstract refinements on data families are lost

[rosekunkel]

The following code is incorrectly declared Safe:

{-# LANGUAGE GADTs, TypeFamilies #-}
module Select where

data family Foo a :: * -> *

{-@
data Foo Int b <p :: String -> Bool> where
  Bar :: Foo<{\v -> len v == 0}> Int ()
@-}
data instance Foo Int b where
  Bar :: Foo Int ()

{-@
upgradeBar :: Foo<{\v -> False}> Int ()
@-}
upgradeBar :: Foo Int ()
upgradeBar = Bar

However, the corresponding code without data families is correctly declared Unsafe:

{-# LANGUAGE GADTs #-}
module Select where

{-@
data Foo a b <p :: String -> Bool> where
  Bar :: Foo<{\v -> len v == 0}> Int ()
@-}
data Foo a b where
  Bar :: Foo Int ()

{-@
upgradeBar :: Foo<{\v -> False}> Int ()
@-}
upgradeBar :: Foo Int ()
upgradeBar = Bar

Error: Liquid Type Mismatch

 15 | upgradeBar = Bar
      ^^^^^^^^^^^^^^^^

   Inferred type
     VV : {v : [GHC.Types.Char] | len v == 0
                                  && len v >= 0}

   not a subtype of Required type
     VV : {VV : [GHC.Types.Char] | GHC.Types.False}

[ranjitjhala]

Am not surprised — don’t even know how this particular language feature works (is a “data family” even represented as a “tycon” ...?) ie what their semantics are.

But at very least LH should complain about unknown tycon.

Why do we need this feature?

On Sat, Jun 8, 2019 at 4:23 PM Rose Kunkel notifications@github.com wrote:

The following code is incorrectly declared Safe:

{-# LANGUAGE GADTs, TypeFamilies #-}module Select where data family Foo a :: ->

{-@data Foo Int b <p :: String -> Bool> where Bar :: Foo<{\v -> len v == 0}> Int () @-}data instance Foo Int b where Bar :: Foo Int ()

{-@upgradeBar :: Foo<{\v -> False}> Int () @-}upgradeBar :: Foo Int () upgradeBar = Bar

However, the corresponding code without data families is correctly declared Unsafe:

{-# LANGUAGE GADTs #-}module Select where

{-@data Foo a b <p :: String -> Bool> where Bar :: Foo<{\v -> len v == 0}> Int () @-}data Foo a b where Bar :: Foo Int ()

{-@upgradeBar :: Foo<{\v -> False}> Int () @-}upgradeBar :: Foo Int () upgradeBar = Bar

Error: Liquid Type Mismatch

15 | upgradeBar = Bar ^^^^^^^^^^^^^^^^

Inferred type VV : {v : [GHC.Types.Char] | len v == 0 && len v >= 0}

not a subtype of Required type VV : {VV : [GHC.Types.Char] | GHC.Types.False}

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1507?email_source=notifications&email_token=AAMS4OD7KXMK5YJUTTOMYZLPZQ5NVA5CNFSM4HWIKBAKYY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4GYNECEQ, or mute the thread https://github.com/notifications/unsubscribe-auth/AAMS4OHHA54WSFVPCGLXNRTPZQ5NVANCNFSM4HWIKBAA .

[ranjitjhala]

As in

1. how data families are needed for Binah

2. Why would it be too tedious to do with plain data types

The above would help clarify both the use case and what it even means to have abstract refinements on data families...

On Sat, Jun 8, 2019 at 4:31 PM Ranjit Jhala jhala@cs.ucsd.edu wrote:

Am not surprised — don’t even know how this particular language feature works (is a “data family” even represented as a “tycon” ...?) ie what their semantics are.

But at very least LH should complain about unknown tycon.

Why do we need this feature?

On Sat, Jun 8, 2019 at 4:23 PM Rose Kunkel notifications@github.com wrote:

The following code is incorrectly declared Safe:

{-# LANGUAGE GADTs, TypeFamilies #-}module Select where data family Foo a :: ->

{-@data Foo Int b <p :: String -> Bool> where Bar :: Foo<{\v -> len v == 0}> Int () @-}data instance Foo Int b where Bar :: Foo Int ()

{-@upgradeBar :: Foo<{\v -> False}> Int () @-}upgradeBar :: Foo Int () upgradeBar = Bar

However, the corresponding code without data families is correctly declared Unsafe:

{-# LANGUAGE GADTs #-}module Select where

{-@data Foo a b <p :: String -> Bool> where Bar :: Foo<{\v -> len v == 0}> Int () @-}data Foo a b where Bar :: Foo Int ()

{-@upgradeBar :: Foo<{\v -> False}> Int () @-}upgradeBar :: Foo Int () upgradeBar = Bar

Error: Liquid Type Mismatch

15 | upgradeBar = Bar ^^^^^^^^^^^^^^^^

Inferred type VV : {v : [GHC.Types.Char] | len v == 0 && len v >= 0}

not a subtype of Required type VV : {VV : [GHC.Types.Char] | GHC.Types.False}

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1507?email_source=notifications&email_token=AAMS4OD7KXMK5YJUTTOMYZLPZQ5NVA5CNFSM4HWIKBAKYY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4GYNECEQ, or mute the thread https://github.com/notifications/unsubscribe-auth/AAMS4OHHA54WSFVPCGLXNRTPZQ5NVANCNFSM4HWIKBAA .

[rosekunkel]

Data families come from Yesod. For a model like

User
  Id Int
  Name String
  Friend Int
  SSN String

Yesod generates code that looks something like

class PersistEntity record where
  data EntityField record :: * -> *

data User = User
  { userId :: Int
  , userName :: String
  , userFriend :: Int
  , userSSN :: String
  }

instance PersistEntity User where
  data EntityField User field where
    UserId :: EntityField User Int
    UserName :: EntityField User String
    UserFriend :: EntityField User Int
    UserSSN :: EntityField User String

Our original plan was to specify policies by adding them to the EntityField definition:

{-@
data EntityField User typ <policy :: User -> User -> Bool> where
  UserId :: EntityField <{\row viewer -> True}> _ _
| UserName :: EntityField <{\row viewer -> userId viewer == userFriend row}> _ _
| UserFriend :: EntityField <{\row viewer -> userId viewer == userFriend row}> _ _
| UserSSN :: EntityField <{\row viewer -> userId viewer == userId row}> _ {v:_ | len v == 9}
@-}

And then the project function could have the Haskell type project :: EntityField record typ -> record -> Tagged typ

So projecting would look like project UserName user and the policy of the output would be automatically determined just by looking at the policy attached to the EntityField argument

But if abstract refinements on data families are lost, this won't work, because the policy on EntityField is an abstract refinement on a data family.

[rosekunkel]

I'm not sure if it would be too tedious to do another way, I'll have to experiment with different ways of specifying the policy for each field.

[nikivazou]

Not sure exactly how data instances work, but before my last push to develop class instances were not checked at all, so maybe this also is fixed?

[rosekunkel]

I tried updating but it's still broken.

My understanding of data families is that data instances are translated into plain data types, and then an axiom is added which says that that plain data type is equal to the data family instance type. So the translation would be something like this:

data family Foo a :: * -> *

data FooInt b where
  Bar :: FooInt ()

axiom FooInt = Foo Int

upgradeBar :: Foo Int ()
upgradeBar = Bar

The core is not very consistent on whether functions like upgradeBar get the type Foo Int () or the type FooInt (), it seems to variously pick both options.

[rosekunkel]

There's some GHC documentation that describes the desugaring in more detail here: https://gitlab.haskell.org/ghc/ghc/wikis/type-functions-core#desugaring-indexed-data-types