Odd error

[Icelandjack]

{-# Language GADTs, RankNTypes, KindSignatures, DataKinds #-}

import GHC.TypeLits
import GHC.Types

{-@ data Monoid a = M @-}
data Mon (a :: Symbol) where
  M :: Mon a

{-@ reflect e @-}
e :: forall (a :: Symbol). KnownSymbol a => Mon a
e = M

{-@ reflect >< @-}
(><) :: forall (a :: Symbol). KnownSymbol a => Mon a -> Mon a -> Mon a
M >< M = M

gives an odd error,

$ liquid --diff tI2C.hs
LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.

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

**** DONE:  Extracted Core using GHC *******************************************

**** DONE:  Transformed Core ***************************************************

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

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

 <no location info>: Error: Uh oh.
     strengthen on differently shaped reftypes 
t1 = {lq_tmp$x##40 : (Mon a)^"lq_tmp$x##28" | lq_tmp$x##40 == ds_d1Ky} [shape = (Mon a)]
t2 = (Monoid a) [shape = (Monoid a)]

Changing Monoid to say Monoidd and it gives a more expected result

$ liquid --diff tI2C.hs
LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.

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

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

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

 /tmp/tI2C.hs:6:10: Error: GHC Error

 6 | {-@ data Monoidd a = M @-}
              ^

     Not in scope: type constructor or class `Monoidd'

[Icelandjack]

Correct version is {-@ data Mon a = M @-}.

[nikivazou]

Thanks for the report @Icelandjack!

BTW, you can refer to the type level literal a as if it was a string in your refinements! See https://github.com/nikivazou/verified_string_matching/blob/master/src/Data/StringMatching/StringMatching.hs#L17

[Icelandjack]

That's cool @nikivazou, thank you for your work on this :) LiquidHaskell is full of goodies.

Is it LiquidHaskell or Liquid Haskell? I've seen both.

[nikivazou]

Thanks @Icelandjack!

I am switching from LiquidHaskell to Liquid Haskell, but have been using both :(