ucsd-progsys / liquidhaskell-tutorial

Tutorial for LiquidHaskell
https://ucsd-progsys.github.io/liquidhaskell-tutorial/
MIT License
75 stars 27 forks source link

divide function in Chapter 3 #74

Open mhwombat opened 5 years ago

mhwombat commented 5 years ago

I have copied and pasted this code from Chapter 3. I believe it should be OK, but LiquidHaskell doesn't like it. Have I misunderstood something, or is this a bug in the tutorial or in LiquidHaskell?

BTW, thank you for the tutorial. It's well-written.

{-@ LIQUID "--no-termination" @-}

{-@ type NonZero = {v:Int | v /= 0} @-}

{-@ die :: {v:String | false} -> a  @-}
die msg = error msg

{-@ divide :: Int -> NonZero -> Int @-}
divide _ 0 = die "divide by zero"
divide n d = n `div` d
$ liquid amy2.hs
LiquidHaskell Version 0.8.4.0, Git revision 57213512a9d69093c12d644b21dbf9da95811894
Copyright 2013-18 Regents of the University of California. All Rights Reserved.

**** DONE:  A-Normalization ****************************************************                                             

**** DONE:  annotate ***********************************************************                                             

**** RESULT: ERROR *************************************************************                                             

 /home/amy/liquidhaskell-tutorial/amy2.hs:8:15-36: Error: Specified type does not refine Haskell type for `Main.divide` (Plugged Init types old)

 8 | {-@ divide :: Int -> NonZero -> Int @-}
                   ^^^^^^^^^^^^^^^^^^^^^^

 The Liquid type

     GHC.Types.Int
     -> GHC.Types.Int
        -> GHC.Types.Int

 is inconsistent with the Haskell type

     forall p -> GHC.Real.Integral p => p -> p -> p

 defined at /home/amy/liquidhaskell-tutorial/amy2.hs:9:1-6

 Specifically, the Liquid component

     GHC.Types.Int

 is inconsistent with the Haskell component

     p

 HINT: Use the hole '_' instead of the mismatched component (in the Liquid specification)
mhwombat commented 5 years ago

Ah, looking through the issues for LiquidHaskell (not the tutorial), I found https://github.com/ucsd-progsys/liquidhaskell/issues/1297. I think the type signature divide :: Int -> Int -> Int should be added to the divide function in the tutorial.