Sort Error in Refinement with imports

[jprider63]

@nikivazou asked me to create this. I have the following signature in Program.hs:

{-@ evalProgramStar :: Pair Index Program -> Pair Index (Program <{\v -> isValue v}>) @-}

In a separate module (Simulations.hs) that imports Program.hs, I get the following error when running liquid on Simulations.hs:

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

 /Users/james/Documents/Projects/lmonad-meta/src/src/Programs.hs:90:13-27: Error: Illegal type specification for `measure Programs.evalProgramStar`

 90 | {-@ reflect evalProgramStar @-}
                  ^^^^^^^^^^^^^^^

     measure Programs.evalProgramStar :: x1:(Pair Integer Program) -> {VV : (Pair Integer {VV : Program | Language.isValue VV}) | VV == Programs.evalProgramStar x1}
     Sort Error in Refinement: {VV : Programs.Program | Language.isValue VV}
     Cannot unify Language.Term with Programs.Program in expression: Language.isValue VV

 /Users/james/Documents/Projects/lmonad-meta/src/src/Programs.hs:90:13-27: Error: Illegal type specification for `assumed type Programs.evalProgramStar`

 90 | {-@ reflect evalProgramStar @-}
                  ^^^^^^^^^^^^^^^

     assumed type Programs.evalProgramStar :: x1:(Pair Integer Program) -> {VV : (Pair Integer {VV : Program | Language.isValue VV}) | VV == Programs.evalProgramStar x1}
     Sort Error in Refinement: {VV : Programs.Program | Language.isValue VV}
     Cannot unify Language.Term with Programs.Program in expression: Language.isValue VV

Dropping the isValue runs fine:

{-@ evalProgramStar :: Pair Index Program -> Pair Index Program @-}

I'm running c607f625849f90cb6ef472f198e8fc96d6e9b69b.

[jprider63]

I also forgot, isValue is defined in Language.hs, which is imported by Program.hs:

isValue :: Term -> Bool
{-@ reflect isValue @-}

[ranjitjhala]

Can you paste the source? Hard to tell what's going on otherwise.

Also: are Program and Term aliases?

On Tue, Oct 24, 2017 at 3:14 PM JP notifications@github.com wrote:

I also forgot, isValue is defined in Language.hs, which is imported by Program.hs:

isValue :: Term -> Bool {-@ reflect isValue @-}

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1145#issuecomment-339150256, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOPbJqj-ZgvEnfChx6rwp5gEyNuHkks5svmBzgaJpZM4QFCm6 .

[jprider63]

I'll try to make a minimal example. No, they're ADTs.

[nikivazou]

I agree with James that it is not straightforward to create a small example that fires this.

The problem is that at client Program <{\v -> isValue v}> is an abstract refinement instantiation on Program

data Program <p :: Expr -> Bool > = Pg { ...,  pgExr :: Expr <p>, ...}

But the import things that isValue refines Programs from the type error

Pair Integer {VV : Program | Language.isValue VV}`

I will try too to generate a minimum program that fires the bug, but not sure when.

[ranjitjhala]

Well is it even a problem with imports? Or does it happen on a single file too?

On Wed, Oct 25, 2017 at 5:29 AM Niki Vazou notifications@github.com wrote:

I agree with James that it is not straightforward to create a small example that fires this.

The problem is that at client Program <{\v -> isValue v}> is an abstract refinement instantiation on Program

data Program <p :: Expr -> Bool > = Pg { ..., pgExr :: Expr

, ...}

But the import things that isValue refines Programs from the type error

Pair Integer {VV : Program | Language.isValue VV}`

I will try too to generate a minimum program that fires the bug, but not sure when.

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1145#issuecomment-339313623, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuODzM8T_P29V6YJ0HA0LT_tUkAqiUks5svymMgaJpZM4QFCm6 .

[nikivazou]

It is related to imports. The functionevalProgramStar with the abstract refinements type checks properly when checked.

But when imported its signature is parsed wrong (ad described above).

On Wed, Oct 25, 2017 at 11:16 AM, Ranjit Jhala notifications@github.com wrote:

Well is it even a problem with imports? Or does it happen on a single file too?

On Wed, Oct 25, 2017 at 5:29 AM Niki Vazou notifications@github.com wrote:

I agree with James that it is not straightforward to create a small example that fires this.

The problem is that at client Program <{\v -> isValue v}> is an abstract refinement instantiation on Program

data Program <p :: Expr -> Bool > = Pg { ..., pgExr :: Expr

, ...}

But the import things that isValue refines Programs from the type error

Pair Integer {VV : Program | Language.isValue VV}`

I will try too to generate a minimum program that fires the bug, but not sure when.

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/ 1145#issuecomment-339313623, or mute the thread https://github.com/notifications/unsubscribe- auth/ABkuODzM8T_P29V6YJ0HA0LT_tUkAqiUks5svymMgaJpZM4QFCm6

.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1145#issuecomment-339364970, or mute the thread https://github.com/notifications/unsubscribe-auth/AArotT2sNYLKYLyiG6MyUH6NwfBL3rdyks5sv1DJgaJpZM4QFCm6 .

-- Niki Vazou

[ranjitjhala]

To be clear, can you show me files F1, F2,... such that

1. When checked separately there is an error,
2. When checked as single (concatenated) module, there is no error?

On Wed, Oct 25, 2017 at 8:39 AM, Niki Vazou notifications@github.com wrote:

It is related to imports. The functionevalProgramStar with the abstract refinements type checks properly when checked.

But when imported its signature is parsed wrong (ad described above).

On Wed, Oct 25, 2017 at 11:16 AM, Ranjit Jhala notifications@github.com wrote:

Well is it even a problem with imports? Or does it happen on a single file too?

On Wed, Oct 25, 2017 at 5:29 AM Niki Vazou notifications@github.com wrote:

I agree with James that it is not straightforward to create a small example that fires this.

The problem is that at client Program <{\v -> isValue v}> is an abstract refinement instantiation on Program

data Program <p :: Expr -> Bool > = Pg { ..., pgExr :: Expr

, ...}

But the import things that isValue refines Programs from the type error

Pair Integer {VV : Program | Language.isValue VV}`

I will try too to generate a minimum program that fires the bug, but not sure when.

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/ 1145#issuecomment-339313623, or mute the thread https://github.com/notifications/unsubscribe- auth/ABkuODzM8T_P29V6YJ0HA0LT_tUkAqiUks5svymMgaJpZM4QFCm6

.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/ 1145#issuecomment-339364970, or mute the thread https://github.com/notifications/unsubscribe-auth/ AArotT2sNYLKYLyiG6MyUH6NwfBL3rdyks5sv1DJgaJpZM4QFCm6 .

-- Niki Vazou

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1145#issuecomment-339373151, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOLrX79gFIlbfZqacm-rtGuHlhFPDks5sv1ZKgaJpZM4QFCm6 .

[ranjitjhala]

It's entirely possible that the import does not properly handle abs-ref; I dont recall any specific tests for it. However, in that case, it should also be possible to create a failing test (simple or otherwise...)

On Wed, Oct 25, 2017 at 8:59 AM, Ranjit Jhala jhala@cs.ucsd.edu wrote:

To be clear, can you show me files F1, F2,... such that

1. When checked separately there is an error,
2. When checked as single (concatenated) module, there is no error?

On Wed, Oct 25, 2017 at 8:39 AM, Niki Vazou notifications@github.com wrote:

It is related to imports. The functionevalProgramStar with the abstract refinements type checks properly when checked.

But when imported its signature is parsed wrong (ad described above).

On Wed, Oct 25, 2017 at 11:16 AM, Ranjit Jhala notifications@github.com wrote:

Well is it even a problem with imports? Or does it happen on a single file too?

On Wed, Oct 25, 2017 at 5:29 AM Niki Vazou notifications@github.com wrote:

I agree with James that it is not straightforward to create a small example that fires this.

The problem is that at client Program <{\v -> isValue v}> is an abstract refinement instantiation on Program

data Program <p :: Expr -> Bool > = Pg { ..., pgExr :: Expr

, ...}

But the import things that isValue refines Programs from the type error

Pair Integer {VV : Program | Language.isValue VV}`

I will try too to generate a minimum program that fires the bug, but not sure when.

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/ 1145#issuecomment-339313623, or mute the thread https://github.com/notifications/unsubscribe- auth/ABkuODzM8T_P29V6YJ0HA0LT_tUkAqiUks5svymMgaJpZM4QFCm6

.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1145# issuecomment-339364970, or mute the thread https://github.com/notifications/unsubscribe-auth/AArotT2sN YLKYLyiG6MyUH6NwfBL3rdyks5sv1DJgaJpZM4QFCm6 .

-- Niki Vazou

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1145#issuecomment-339373151, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOLrX79gFIlbfZqacm-rtGuHlhFPDks5sv1ZKgaJpZM4QFCm6 .

[jprider63]

I spent some time trying to create a minimal example, but haven't had any luck. In the meantime, I've given you access to our repository. You should see the bug if you switch to the refinement on line 92 of src/src/Programs.hs in branch dev.jp.

[ranjitjhala]

@jprider63 can you tell me the exact set of steps to reproduce the bug? as in, after:

1. git clone ... 
2. git checkout ... 
3. stack exec -- liquid ???

what is the exact ??? that I should run LH on?

[jprider63]

After you git checkout dev.jp, uncomment line 92 and comment line 93. Then you can just run make (which is the same as cd src/src && liquid ProofCombinators.hs && liquid Label.hs && liquid Language.hs && liquid Programs.hs).