Type inconsistency

[marciocornelio]

Hi, I am using

LiquidHaskell Version 0.8.2.4, Git revision 9f30411
Copyright 2013-18 Regents of the University of California. All Rights Reserved.

I am doing the examples of one tutorial, and I have faced a problem with the following example

{-@ 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

When checking it with LiquidHaskell, I get the following error.

_Error: Specified type does not refine Haskell type for `Main.divide` (Plugged Init types)

 130 | {-@ divide :: Int -> NonZero -> Int @-}
                     ^^^^^^^^^^^^^^^^^^^^^^
 The Liquid type
     Int -> Int -> Int
 is inconsistent with the Haskell type
     forall p -> GHC.Real.Integral p => p -> p -> p_

Do we have any workaround? Any hints? Thank you.

[ranjitjhala]

Hi @marciocornelio -- yes the issue here is that GHC thinks that the type is the (more general)

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

because there is no explicit type signature. The solution is simply to put in the GHC type signature,

{-@ type NonZero = {v:Int | v /= 0} @-}
{-@ die :: {v:String | false} -> a  @-}
die msg = error msg

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