Ah of course, I always forget that we can assign specs to vars in other
modules :)

This looks good to me then, feel free to merge.


On Tue, Oct 1, 2013 at 1:15 PM, Niki Vazou <notifications@github.com> wrote:

> In Language/Haskell/Liquid/Bare.hs:
>
> >    = inModule mod $ makeAssumeSpec' cfg vs $ Ms.sigs spec
> >
> > +makeLocalAssumeSpec :: Config -> ModName -> [Var] -> [Var] -> [(LocSymbol, BareType)]
> > +                    -> BareM [(ModName, Var, Located SpecType)]
> > +
> > +makeLocalAssumeSpec cfg mod vs lvs xbs
> > +  = do env     <- get
> > +       let vbs1 = expand3 <$> varSymbols fchoose "Var" lvs (dupSnd <$> xbs1)
> > +       when (not $ noCheckUnknown cfg) $
> > +         checkDefAsserts env vbs1 xbs1
> > +       vts1    <- map (addFst3 mod) <$> mapM mkVarSpec vbs1
>
> Correct,
> Unlikely, xbs2 is not empty, if you see my the commits, I added it for
>
> +Failed 3 tests:
>
>    - ../benchmarks/bytestring-0.9.2.1/Data/ByteString.split.1.T.hs,
>    - ../benchmarks/bytestring-0.9.2.1/Data/ByteString.split.1.hs,
>    - ../benchmarks/text-0.11.2.3/Data/Text/Foreign.hs
>
> If you have a more elegant solution, it is wellcome
>
> —
> Reply to this email directly or view it on GitHub<https://github.com/ucsd-progsys/liquidhaskell/pull/128/files#r6697959>
> .
>