Errors following examples in tutorial

[Tomas Diaz]

Hello, 

I was following the tutorial (http://ucsd-progsys.github.io/liquidhaskell-tutorial/) and I kept getting some errors with some of the examples shown in there, which I eventually fixed but I am not sure if it was normal or not...  Maybe the examples are not updated or it's something to do with my GHC version (or maybe something else).

For example, in page 30, there is:

{-@ divide :: Int -> NonZero -> Int @-}
divide _ 0 = die "divide by zero"
divide n d = n  `div`  d

I got the error:

Which I fixed by specifying the type, as follows:

{-@ divide :: Int -> NonZero -> Int @-}

divide _ 0= die "divide by zero"

divide n d = (n :: Int) `div`  (d :: Int)

Same goes with the example in page 31, "abs" where I have to use the :: Int. (There are other examples as well, but similar in the error)

I'm working on a Mac OS X Sierra, using GHC 7.10.3 and z3 version 4.5.

Thank you in advance!

Tomás

[Niki Vazou]

Thanks Tomas! 

There are some Haskell type specs in the tutorial that are hidden to keep the tutorial simple. 

--
You received this message because you are subscribed to the Google Groups "liquidhaskell" group.
To unsubscribe from this group and stop receiving emails from it, send an email to liquidhaskell+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--

Niki

[Ranjit Jhala]

Hi Tomas,

Did you fork the repo or type in the code into a blank file yourself? If the latter you will get these problems as GHC infers a most general type that is different from the liquid one. In the repo version of the file we also have the Haskell type but that is omitted from the PDF/HTML for brevity.

In retrospect this was a mistake, I will add those back in for folks who are typing in themselves (which, frankly is the better route!) but for now you can add the Haskell type signatures or get them from the repo.

Does this help?

Thanks!

Ranjit.

To unsubscribe from this group and stop receiving emails from it, send an email to liquidhaskel...@googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

--

Niki

--

You received this message because you are subscribed to the Google Groups "liquidhaskell" group.

To unsubscribe from this group and stop receiving emails from it, send an email to liquidhaskel...@googlegroups.com.

[Tomas Diaz]

Oooh ok ! Thank you! :) 

(Yep, I was typing them myself haha)