make functor a generic class for #1619

[nikivazou]

So, in @rosekunkel 's example, the abstract refinement label was defaulted to true because Functor is not "generic", so no fresh type was created.

@rosekunkel this fixes your issue, but if you want to have similar behavior on other type classes, you should make a similar edit and add, e.g., applicative, monads, etc in the generic set, like I did.

@ranjitjhala I am not entirely sure that Functor (and the rest type constructors) are generic. It would be cool to formalize what generic means for such constructors. But the truth is, we are being too strict by not refreshing at all non generic types. I suspect we need to refresh the inner parts of the type (as here) but not the top level refinements.

Anyway, this should unblock Rose.

[ranjitjhala]

Instead of hacking “isGeneric” this way why Not use abstract refinements on the signature of Fmap?

…

On Mon, Feb 24, 2020 at 4:26 AM Niki Vazou ***@***.***> wrote: @nikivazou <https://github.com/nikivazou> requested your review on: #1621 <#1621> make functor a generic class for #1619 <#1619>. — You are receiving this because your review was requested. Reply to this email directly, view it on GitHub <#1621?email_source=notifications&email_token=AAMS4OGW3H5XT7UTCGMHKK3REO4FPA5CNFSM4K2FST22YY3PNVWWK3TUL52HS4DFWZEXG43VMVCXMZLOORHG65DJMZUWGYLUNFXW5KTDN5WW2ZLOORPWSZGOW2ZJ4AY#event-3065159171>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAMS4OHPIIVNG5MNV6HDXGDREO4FPANCNFSM4K2FST2Q> .

[nikivazou]

Good question :)
Did you try it?

[nikivazou]

ok, @ranjitjhala you are suggesting to add an abstract refinement

1. in a class method (I don't think we support that :) )[1]
2. in a type variable for a type constructor (I don't think we support that either)[2]

I suggest, if this blocking Rose to hack isGeneric, otherwise properly fix it but this would need time.

[1] The following creates a parse error

{-@ class Functor f where
  fmap :: forall <p :: f -> Prop>. (a -> b) -> f a -> f b
  (<$) :: forall a b. a -> f b -> f a
  @-}

[2] The following creates a parse error

{-@   fmap'' :: forall <p :: f -> Bool>. (a -> b) -> (f<p>) a -> (f<p>) b @-}
fmap'' :: (a -> b) -> f a -> f b 
fmap''   = undefined

[ranjitjhala]

How about just an assume for the signature of fmap?

…

On Mon, Feb 24, 2020 at 9:39 AM Niki Vazou ***@***.***> wrote: ok, @ranjitjhala <https://github.com/ranjitjhala> you are suggesting to add an abstract refinement 1. in a class method (I don't think we support that :) )[1] 2. in a type variable for a type constructor (I don't think we support that either)[2] I suggest, if this blocking Rose to hack isGeneric, otherwise properly fix it but this would need time. [1] The following creates a parse error {-@ class Functor f where fmap :: forall <p :: f -> Prop>. (a -> b) -> f a -> f b (<$) :: forall a b. a -> f b -> f a @-} [2] The following creates a parse error {-@ fmap'' :: forall <p :: f -> Bool>. (a -> b) -> (f<p>) a -> (f<p>) b @-} fmap'' :: (a -> b) -> f a -> f b fmap'' = undefined — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#1621?email_source=notifications&email_token=AAMS4OASOEH42BOSFJ6JZ63REQA5NA5CNFSM4K2FST22YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEMY2VKI#issuecomment-590457513>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAMS4OGD2DROMRNEMSG7YBLREQA5NANCNFSM4K2FST2Q> .

[nikivazou]

We still have problem number 2.

[ranjitjhala]

@nikivazou why was this not merged in? (I can't tell by reading the comments but somehow this PR was closed?)