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 <[email protected]> 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> .

[nikivazou]

I suspect so, but you would need to say that Monad is generic type class.
From that, it would not suffice to add abstract refinements only to fmap, but to many more methods.

[ranjitjhala]

Yes, I was including Monad etc. too...

…

On Wed, Feb 26, 2020 at 11:41 AM Niki Vazou ***@***.***> wrote: I suspect so, but you would need to say that Monad is generic type class. From that, it would not suffice to add abstract refinements only to fmap, but to many more methods. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#1619?email_source=notifications&email_token=AAMS4ODRZ5KJ7C4OL77H753RE3ATZA5CNFSM4KZPUIB2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOENBTHYA#issuecomment-591606752>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAMS4OF4TUUMRJHJN5GDBI3RE3ATZANCNFSM4KZPUIBQ> .