ignoring InstanceSigs

[mutjida]

Liquid Haskell seems to be ignoring {-# LANGUAGE InstanceSigs #-}.

Here is a contrived example:

{-# LANGUAGE InstanceSigs #-}

{-@ data Nt = Nt {getNt :: {v:Int | v >= 0}} @-}

data Nt = Nt Int

{-@ natPlus :: {x:Nt | getNt x > 0} -> Nt -> Nt @-}

natPlus :: Nt -> Nt -> Nt

natPlus (Nt x) (Nt y) = Nt (x + y)

instance Monoid Nt where

    mempty = Nt 0

    {-@ mappend :: {x:Nt | getNt x > 0} -> Nt -> Nt @-}

    mappend :: Nt -> Nt -> Nt

    mappend = natPlus

which produces the following Liquid Haskell error:

 Data/Monoid/LqdBug.hs:12:9-15: Error: Specified Type Does Not Refine Haskell Type for GHC.Base.mappend

 

 12 |     {-@ mappend :: {x:Nt | getNt x > 0} -> Nt -> Nt @-}

              ^^^^^^^

 

 The Liquid type

  

     Main.Nt -> Main.Nt -> Main.Nt

  

 is inconsistent with the Haskell type

  

     forall a. GHC.Base.Monoid a => a -> a -> a

  

 defined at <no location info>

Is this error intentional?

thanks,

  Jeff

[Ranjit Jhala]

Interesting -- I didn't know about this LANGUAGE pragma; 

its entirely likely that LH is ignoring it. 

Thanks for pointing it out!

That said, I'm not sure LH has any machinery to allow for 

"per instance" refinements like the above (where the instance

for `Nt` has different (refined) type compared to the generic 

`Monoid` signature.

This is somewhat of an open problem, as I _think_ it requires

some form of intersection types.

What was your use case? This could provide some motivation for

buttoning down and solving this problem!

Thanks!

--
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.
For more options, visit https://groups.google.com/d/optout.

[jeff p]

I am creating a monoidal datatype which is parameterized on a string value, which I'll call the seed. I want to use Liquid Haskell to prove some invariants on my datatype which depend on the seed. Initially I used type level strings to make sure that only compatible values could be combined. However, since LH can't see type level strings, I added the term level copies of the seed to my datatype constructors (as you suggested). Now, in order to prove my invariants, LH needs to know that the seed values of each argument to mappend are the same; so I added a constraint to the function I am using for mappend. 

[Niki Vazou]

We do have a limited support for per instance refinements!

Here is how you can write your example 

http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1458637873_6430.hs

The definition of mapped as `mappend = natPlus` currently throws an error, but will look into it ASAP.

Ranjit, we do not exactly use intersection types, but instead we curry around a mapping from dictionaries to their refined specifications and each time we instantiate a dictionary we look up the mapping if any refinement type exists the the specific instantiation. 

Best, 

 

--

Niki Vazou