Ch 4: Cannot unify Data.Vector.Vector with Data.Vector.Generic.Base.Vector

[mpdairy]

Hi, I can't get VectorN to work for twoLangs in the example from chapter 4.

Here's a condensed version of my code:

{-@ LIQUID "--reflection" @-}

module Blaze.Liquid.Ex4 where

import Prelude hiding (abs)
import Data.Vector (Vector, (!))
import qualified Data.Vector as V

{-@ type VectorN a N = {v:Vector a | vlen v == N} @-}

{-@ twoLangs :: VectorN String 2 @-}
twoLangs  = V.fromList ["haskell", "javascript"]

and here's the error I get:

Error: Specified type does not refine Haskell type for `Blaze.Liquid.Ex4.twoLangs` (Checked)

 53 | {-@ twoLangs :: VectorN String 2 @-}
                      ^^^^^^^^^^^^^^^^^

 The Liquid type

     Data.Vector.Generic.Base.Vector [GHC.Types.Char]

 is inconsistent with the Haskell type

     Data.Vector.Vector [GHC.Types.Char]

 defined at /home/matt/haskell/blaze/src/Blaze/Liquid/Ex4.hs:55:1-8

 /home/matt/haskell/blaze/src/Blaze/Liquid/Ex4.hs:53:17-33: Error: Illegal type specification for `Blaze.Liquid.Ex4.twoLangs`

 53 | {-@ twoLangs :: VectorN String 2 @-}
                      ^^^^^^^^^^^^^^^^^

     Blaze.Liquid.Ex4.twoLangs :: {VV : (Data.Vector.Generic.Base.Vector [GHC.Types.Char]) | vlen VV == 2}
     Sort Error in Refinement: {VV##0 : (Data.Vector.Generic.Base.Vector [Char]) | vlen VV##0 == 2}
     Cannot unify Data.Vector.Vector with Data.Vector.Generic.Base.Vector in expression: vlen VV##0 

I tried importing Vector from Data.Vector.Generic.Base but that didn't work either.

I'm running liquid haskell with the command:

stack exec -- liquid src/Blaze/Liquid/Ex4.hs

[ranjitjhala]

Hi @mpdairy ,

sorry, this is because of some unfortunate name resolution issues we've had with the GHC API -- specifically in the alias

{-@ type VectorN a N = {v:Vector a  | vlen v == N} @-}

the name Vector is resolving to the "wrong" thing.

There are two possible fixes.

1. Use the qualified name V.Vector in the alias, i.e. make it:

{-@ type VectorN a N = {v : V.Vector a  | vlen v == N} @-}

2. Better still, replace the name with a hole and let LH+GHC automatically fill it in:

{-@ type VectorN a N = {v : _  | vlen v == N} @-}

Either of those should work, can you confirm?

Thanks!

[mpdairy]

Thanks, both of those options worked!