Skip to content

divide function in Chapter 3 #74

@mhwombat

Description

@mhwombat

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)

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions