Polymorphic instantiation seems broken with typeclasses

[rosekunkel]

Liquid deems fmapPreservesLabel unsafe, but its equivalent using explicit dictionary passing, myFmapPreservesLabel, is deemed safe. They should both be safe, since fmap/myFmap should be instantiated at Tagged Label<label>.

{-# LANGUAGE Rank2Types #-}

{-@ data Label<label :: User -> Bool> where @-}
data Label
data User
data Tagged l a = Tag a
data MyFunctor f = MyFunctor { myFmap :: forall a b. (a -> b) -> f a -> f b }

instance Functor (Tagged l) where
  fmap = fmapTagged

taggedFunctor :: MyFunctor (Tagged l)
taggedFunctor = MyFunctor fmapTagged

fmapTagged :: (a -> b) -> Tagged l a -> Tagged l b
fmapTagged f (Tag x) = Tag (f x)

{-@
myFmapPreservesLabel :: forall <label :: User -> Bool>.
(a -> b) -> Tagged (Label<label>) a -> Tagged (Label<label>) b
@-}
myFmapPreservesLabel :: (a -> b) -> Tagged Label a -> Tagged Label b
myFmapPreservesLabel = myFmap taggedFunctor

{-@
fmapPreservesLabel :: forall <label :: User -> Bool>.
(a -> b) -> Tagged (Label<label>) a -> Tagged (Label<label>) b
@-}
fmapPreservesLabel :: (a -> b) -> Tagged Label a -> Tagged Label b
fmapPreservesLabel = fmap

[ranjitjhala]

I don’t think it’s the type class, more likely the HKT — LH is (probably) not doing any polymorphic instantiation when argument used in the type application is NOT of kind * Ie it ONLY does instantiation when the type IS of kind * (that’s my guess.) GHC desugars the fmap into fmap @ Tagged Label @ a @ b And my guess is LH is not doing any instantiation for the Tagged Label. I wonder why the other version passes... maybe because LH instantiates the l in the sig for the dictionary?

…

On Sat, Feb 22, 2020 at 12:25 AM Rose Kunkel ***@***.***> wrote: Liquid deems fmapPreservesLabel unsafe, but its equivalent using explicit dictionary passing, myFmapPreservesLabel, is deemed safe. They should both be safe, since fmap/myFmap should be instantiated at Tagged Label<label>. {-# LANGUAGE Rank2Types #-} {-@ data Label<label :: User -> Bool> where @-}data Labeldata Userdata Tagged l a = Tag adata MyFunctor f = MyFunctor { myFmap :: forall a b. (a -> b) -> f a -> f b } instance Functor (Tagged l) where fmap = fmapTagged taggedFunctor :: MyFunctor (Tagged l) taggedFunctor = MyFunctor fmapTagged fmapTagged :: (a -> b) -> Tagged l a -> Tagged l b fmapTagged f (Tag x) = Tag (f x) ***@***.*** :: forall <label :: User -> Bool>. (a -> b) -> Tagged (Label<label>) a -> Tagged (Label<label>) b @-}myFmapPreservesLabel :: (a -> b) -> Tagged Label a -> Tagged Label b myFmapPreservesLabel = myFmap taggedFunctor ***@***.*** :: forall <label :: User -> Bool>. (a -> b) -> Tagged (Label<label>) a -> Tagged (Label<label>) b @-}fmapPreservesLabel :: (a -> b) -> Tagged Label a -> Tagged Label b fmapPreservesLabel = fmap — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#1619?email_source=notifications&email_token=AAMS4OFGV67E77BJYSGCARTREDONTA5CNFSM4KZPUIB2YY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4IPO3T5Q>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAMS4OBUQN6DK4MPG256HWLREDONTANCNFSM4KZPUIBQ> .

[rosekunkel]

I should mention that this is currently blocking my attempt to rewrite Binah in the MAC style. (Well, not blocking exactly, but it means none of the code can use do-notation or monad transformers, which is very unfortunate).

[ranjitjhala]

@niki vazou <nikivazou@gmail.com> any chance you can look at this soon? I think it's either really easy or really hard to add this feature :-) (btw, why should do notation come into play here? Looks like the problem is with fmap? or is it that the issue is just a simplification and the problem also arises with the type of >>= etc.?)

[rosekunkel]

It also happens with >>= (and I think basically every HKT typeclass).

[jprider63]

I'm not sure if this is helpful, but Yiyun, Niki, and I are close to getting typeclasses working. Functor seems to mostly work, but there are a few issues we're still resolving. We can share the branch when it's fully working.

[nikivazou]

@rosekunkel, it looks indeed like an instantiation problem. The below is SAFE. Would that unblock you, or should I look deeper?

{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE FlexibleInstances #-}

{-@ data Label<label :: User -> Bool> where @-}
data Label
data User
data Tagged l a = Tag a
data MyFunctor f = MyFunctor { myFmap :: forall a b. (a -> b) -> f a -> f b }

instance Functor (Tagged Label) where
{-@ instance Functor (Tagged Label) where 
    fmap :: forall <label :: User -> Bool>. (a -> b) -> Tagged (Label<label>) a -> Tagged (Label<label>) b
    @-}
  fmap = fmapTagged

fmapTagged :: (a -> b) -> Tagged l a -> Tagged l b
fmapTagged f (Tag x) = Tag (f x)


{-@
fmapPreservesLabel :: forall <label :: User -> Bool>.
(a -> b) -> Tagged (Label<label>) a -> Tagged (Label<label>) b
@-}
fmapPreservesLabel :: (a -> b) -> Tagged Label a -> Tagged Label b
fmapPreservesLabel = fmap

[rosekunkel]

That technically unblocks me, but it removes a lot of the advantage of using the MAC encoding over the current one - since the type of `>>=` will have to be similarly refined, we can't treat `Tagged Label` as a normal monad. So all the monad combinators won't preserve the label automatically, which they would by polymorphism for `Tagged l`.

…

On Sun, Feb 23, 2020, 23:37 Niki Vazou ***@***.***> wrote: @rosekunkel <https://github.com/rosekunkel>, it looks indeed like an instantiation problem. The below is SAFE. Would that unblock you, or should I look deeper? {-# LANGUAGE Rank2Types #-} {-# LANGUAGE FlexibleInstances #-} {-@ data Label<label :: User -> Bool> where @-} data Label data User data Tagged l a = Tag a data MyFunctor f = MyFunctor { myFmap :: forall a b. (a -> b) -> f a -> f b } instance Functor (Tagged Label) where {-@ instance Functor (Tagged Label) where fmap :: forall <label :: User -> Bool>. (a -> b) -> Tagged (Label<label>) a -> Tagged (Label<label>) b @-} fmap = fmapTagged fmapTagged :: (a -> b) -> Tagged l a -> Tagged l b fmapTagged f (Tag x) = Tag (f x) {-@ fmapPreservesLabel :: forall <label :: User -> Bool>. (a -> b) -> Tagged (Label<label>) a -> Tagged (Label<label>) b @-} fmapPreservesLabel :: (a -> b) -> Tagged Label a -> Tagged Label b fmapPreservesLabel = fmap — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#1619?email_source=notifications&email_token=AAKWSXGGYH4M6YEXKWOPIBDREN2NNA5CNFSM4KZPUIB2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEMW3I2Q#issuecomment-590197866>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAKWSXHWP6KVDS4WRSFEYNTREN2NNANCNFSM4KZPUIBQ> .

[nikivazou]

I am not following your reasoning 100%.
The one encoding is polymorphic over the type l and the other over the abstract refinement l.
So, the encodings seem equivalent.

At any case, I will try to take a deeper look into this later today.

[rosekunkel]

For example, if we tried to use `sequence` on a list of tagged values, sequence would get the type `[Tagged Label a] -> Tagged Label [a]`, not `forall <label :: User -> Bool>. [Tagged Label<label> a] -> Tagged Label<label> [a]`. If instead the monad instance is for `Tagged l`, then sequence would get the type `[Tagged l a] -> Tagged l [a]`, and then `l` could be instantiated with `Label<label>`. In essence your solution tells LH that >>= has a special type for Tagged Label, but what I think we really want is to be able to tell LH that the monad instance for Tagged is really `instance forall <label :: User -> Bool>. Monad (Tagged Label<label>)`. That syntax doesn't exist, though.

…

On Mon, Feb 24, 2020, 00:41 Niki Vazou ***@***.***> wrote: I am not following your reasoning 100%. The one encoding is polymorphic over the type l and the other over the abstract refinement l. So, the encodings seem equivalent. At any case, I will try to take a deeper look into this later today. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#1619?email_source=notifications&email_token=AAKWSXGPKE2IJR6FKBVSAGDREOB4FA5CNFSM4KZPUIB2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEMW7YQA#issuecomment-590216256>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAKWSXELHTQ42P3SWZUFCITREOB4FANCNFSM4KZPUIBQ> .

[nikivazou]

Hmmm interesting.

Ok, I think I got the problem (or a problem...), are you on slack?

[nikivazou]

So, #1621 has a fix for that where the Functor is added in the generic type classes.
The problem might also be solved by adding abstract refinements, which is currently not supported bu LH.

[ranjitjhala]

Btw modifying the isGeneric should also address the “sequence” issue right?

…

On Tue, Feb 25, 2020 at 10:09 AM Niki Vazou ***@***.***> wrote: So, #1621 <#1621> has a fix for that where the Functor is added in the generic type classes. The problem might also be solved by adding abstract refinements, which is currently not supported bu LH. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#1619?email_source=notifications&email_token=AAMS4ODGUVAIFIVVU6WLUCDREVNFDA5CNFSM4KZPUIB2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEM4Z7EA#issuecomment-590978960>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAMS4OENI7M6J4VOF6QJH4LREVNFDANCNFSM4KZPUIBQ> .