Explanation / hints for "does not refine Haskell type" error in tutorial

[DestyNova]

Hi, I've been working through the tutorial and enjoying it. In chapter 5, I got stuck for quite a long time on the sparse vector plus exercise. I tried many variations, but kept getting the same error:

Error: Specified type does not refine Haskell type for `RefinedDatatypes.plus` (Plugged Init types old)
The Liquid type
 
    (Num a) -> (Sparse a) -> (Sparse a) -> (Sparse a)
 
is inconsistent with the Haskell type
 
    forall p1 p2 a -> p1 -> p2 -> a
 
defined at /home/rjhala/research/stack/liquid/liquid-server/resources/custom/liquidhaskell/sandbox/1586736919_6704.hs:83:1-4
 
Specifically, the Liquid component
 
    (Sparse a)
 
is inconsistent with the Haskell component
 
    p
 
HINT: Use the hole '_' instead of the mismatched component (in the Liquid specification)

I tried replacing parts of the LH type signature with holes as suggested
After some searching, I found issue #1297 which looked very similar. The solution there was to add an explicit Haskell type as well as the LH type, which solved the problem in that issue. I tried the same thing and it immediately solved the problem for me too:

{-@ plus     :: (Num a) =>
    x:Sparse a ->
    SparseN a (spDim x) ->
    SparseN a (spDim x) @-}
plus :: (Num a) => Sparse a -> Sparse a -> Sparse a    -- needed this line
plus x y = undefined

Could I suggest that some text be added to the tutorial (maybe in chapter 5 where it's likely to happen) so that the reader can know what to expect and how to deal with it? I would do a PR myself but I still don't fully understand why it's necessary to add an explicit Haskell type signature here. My mental model was that LH would automatically emit a Haskell type signature similar to the one I inserted above?

[ranjitjhala]

Very sorry about that! Thanks for the tip I will add the extra text as you suggest!!

…

On Sun, Apr 12, 2020 at 5:22 PM Oisín ***@***.***> wrote: Hi, I've been working through the tutorial and enjoying it. However I got stuck for quite a long time on the sparse vector plus exercise in chapter 5. I tried many variations, but kept getting the same error: Error: Specified type does not refine Haskell type for `RefinedDatatypes.plus` (Plugged Init types old) The Liquid type (Num a) -> (Sparse a) -> (Sparse a) -> (Sparse a) is inconsistent with the Haskell type forall p1 p2 a -> p1 -> p2 -> a defined at /home/rjhala/research/stack/liquid/liquid-server/resources/custom/liquidhaskell/sandbox/1586736919_6704.hs:83:1-4 Specifically, the Liquid component (Sparse a) is inconsistent with the Haskell component p HINT: Use the hole '_' instead of the mismatched component (in the Liquid specification) I tried replacing parts of the LH type signature with holes as suggested After some searching, I found issue #1297 <#1297> which looked very similar. The solution there was to add an explicit Haskell type as well as the LH type, which solved the problem in that issue. I tried the same thing and it immediately solved the problem for me too: {-@ plus :: (Num a) => x:Sparse a -> SparseN a (spDim x) -> SparseN a (spDim x) @-}plus :: (Num a) => Sparse a -> Sparse a -> Sparse a -- needed this line plus x y = undefined Could I suggest that some text be added to the tutorial (maybe in chapter 5 where it's likely to happen) so that the reader can know what to expect and how to deal with it? I would do a PR myself but I still don't fully understand why it's necessary to add an explicit Haskell type signature here. My mental model was that LH would automatically emit a Haskell type signature similar to the one I inserted above? — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#1644>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAMS4OEOQUXLHESTYL3UXC3RMJLKXANCNFSM4MGTZ5JQ> .

[ranjitjhala]

Btw, I should have added:

My mental model was that LH would automatically emit a Haskell type

signature similar to the one I inserted above? No, this is not the case. LH's specifications are always _refinements_ of GHC's. In the above, example, GHC would infer and give `plus` a type like `a -> b -> c` and then LH complains that the refined signature is not, in fact, a refinement of `a -> b -> c`. I think in addition to your suggestion, I will *also* update the error message produced in this "mismatch" case to make the point quite explicit -- e.g. to suggest adding a GHC sig if one is missing! Thanks very much again!

…

On Sun, Apr 12, 2020 at 7:49 PM Ranjit Jhala ***@***.***> wrote: Very sorry about that! Thanks for the tip I will add the extra text as you suggest!! On Sun, Apr 12, 2020 at 5:22 PM Oisín ***@***.***> wrote: > Hi, I've been working through the tutorial and enjoying it. However I got > stuck for quite a long time on the sparse vector plus exercise in > chapter 5. I tried many variations, but kept getting the same error: > > Error: Specified type does not refine Haskell type for `RefinedDatatypes.plus` (Plugged Init types old) > The Liquid type > > (Num a) -> (Sparse a) -> (Sparse a) -> (Sparse a) > > is inconsistent with the Haskell type > > forall p1 p2 a -> p1 -> p2 -> a > > defined at /home/rjhala/research/stack/liquid/liquid-server/resources/custom/liquidhaskell/sandbox/1586736919_6704.hs:83:1-4 > > Specifically, the Liquid component > > (Sparse a) > > is inconsistent with the Haskell component > > p > > HINT: Use the hole '_' instead of the mismatched component (in the Liquid specification) > > I tried replacing parts of the LH type signature with holes as suggested > After some searching, I found issue #1297 > <#1297> which looked > very similar. The solution there was to add an explicit Haskell type as > well as the LH type, which solved the problem in that issue. I tried the > same thing and it immediately solved the problem for me too: > > {-@ plus :: (Num a) => > x:Sparse a -> > SparseN a (spDim x) -> > SparseN a (spDim x) @-}plus :: (Num a) => Sparse a -> Sparse a -> Sparse a -- needed this line > plus x y = undefined > > Could I suggest that some text be added to the tutorial (maybe in chapter > 5 where it's likely to happen) so that the reader can know what to expect > and how to deal with it? I would do a PR myself but I still don't fully > understand why it's necessary to add an explicit Haskell type signature > here. My mental model was that LH would automatically emit a Haskell type > signature similar to the one I inserted above? > > — > You are receiving this because you are subscribed to this thread. > Reply to this email directly, view it on GitHub > <#1644>, or > unsubscribe > <https://github.com/notifications/unsubscribe-auth/AAMS4OEOQUXLHESTYL3UXC3RMJLKXANCNFSM4MGTZ5JQ> > . >

[DestyNova]

Thanks for the helpful explanation 👍