Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.
Sign upLH accepts function with malformed spec #292
Comments
ranjitjhala
added
the
bug
label
Jan 1, 2015
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
ranjitjhala
Jan 2, 2015
Member
Another variant. The actual bugs are different of course, in the latter case I think we probably just take a prefix of the args and drop the rest which is why badspec1.hs is safe.
Silly but very severe bug, we shouldn't be accepting programs with malformed specs!
|
Another variant. The actual bugs are different of course, in the latter case I think we probably just take a prefix of the args and drop the rest which is why Silly but very severe bug, we shouldn't be accepting programs with malformed specs! |
nikivazou
closed this
Jan 3, 2015
nikivazou
reopened this
Jan 3, 2015
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
nikivazou
Jan 3, 2015
Member
I think @spinda (Michael) has a fix for the second variant (not merged yet.)
|
I think @spinda (Michael) has a fix for the second variant (not merged yet.) |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Jan 17, 2015
Member
I believe the cause for the second variant is the same as for #287.
Looking at it again, that looks like a totally different issue. The problem is that it's accepting Foo 1000 instead of Fooz 1000, right?
|
Looking at it again, that looks like a totally different issue. The problem is that it's accepting |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
|
Yes the 1000 is somehow ignored in the application... |
spinda
referenced this issue
Jan 17, 2015
Merged
Generalize graph-based alias expansion; use to expand predicate and expression aliases #310
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
|
Just as an update, I'm working on fixing this right now. |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
ranjitjhala
Mar 27, 2015
Member
Folks, what is going on with this?
We need to fix it ASAP, because its a rather horrible and urgent bug.
I have added another version, this time in tests/neg to remind ourselves
that the build is broken until this is fixed.
|
Folks, what is going on with this? We need to fix it ASAP, because its a rather horrible and urgent bug. I have added another version, this time in |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 27, 2015
Member
Ack, ack, ack. Right, this is the plugHoles issue.
On Fri, Mar 27, 2015, 11:03 Ranjit Jhala notifications@github.com wrote:
Folks, what is going on with this?
We need to fix it ASAP, because its a rather horrible and urgent bug.
I have added another version, this time in tests/neg to remind ourselves
that the build is broken until this is fixed.—
Reply to this email directly or view it on GitHub
#292 (comment)
.
|
Ack, ack, ack. Right, this is the plugHoles issue. On Fri, Mar 27, 2015, 11:03 Ranjit Jhala notifications@github.com wrote:
|
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
ranjitjhala
Mar 27, 2015
Member
Is it the case that plug holes is going to take a while to fix?
On Mar 27, 2015, at 11:05 AM, Michael Smith notifications@github.com wrote:
Ack, ack, ack. Right, this is the plugHoles issue.
On Fri, Mar 27, 2015, 11:03 Ranjit Jhala notifications@github.com wrote:
Folks, what is going on with this?
We need to fix it ASAP, because its a rather horrible and urgent bug.
I have added another version, this time in tests/neg to remind ourselves
that the build is broken until this is fixed.—
Reply to this email directly or view it on GitHub
#292 (comment)
.—
Reply to this email directly or view it on GitHub.
|
Is it the case that plug holes is going to take a while to fix?
|
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 27, 2015
Member
No, I believe it can be fixed on its own. I'll work on it asap if no one
else has gotten to it before then.
On Fri, Mar 27, 2015, 12:54 Ranjit Jhala notifications@github.com wrote:
Is it the case that plug holes is going to take a while to fix?
On Mar 27, 2015, at 11:05 AM, Michael Smith notifications@github.com
wrote:Ack, ack, ack. Right, this is the plugHoles issue.
On Fri, Mar 27, 2015, 11:03 Ranjit Jhala notifications@github.com
wrote:Folks, what is going on with this?
We need to fix it ASAP, because its a rather horrible and urgent bug.
I have added another version, this time in tests/neg to remind
ourselves
that the build is broken until this is fixed.—
Reply to this email directly or view it on GitHub
<
#292 (comment).
—
Reply to this email directly or view it on GitHub.—
Reply to this email directly or view it on GitHub
#292 (comment)
.
|
No, I believe it can be fixed on its own. I'll work on it asap if no one On Fri, Mar 27, 2015, 12:54 Ranjit Jhala notifications@github.com wrote:
|
spinda
self-assigned this
Mar 27, 2015
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 27, 2015
Member
Working on this right now. (Well, first I'm waiting for my system to update so that I can compile the latest fixpoint...)
|
Working on this right now. (Well, first I'm waiting for my system to update so that I can compile the latest |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 27, 2015
Member
For badspec.hs, plugHoles turns
module Goo where
{-@ foo :: xs:_ -> {v:_ | this = rubbish } @-}
foo _ _ = 0into
module Goo where
{-@ foo :: Num a => xs:t -> {v:(t -> a) | this = rubbish } @-}
foo :: Num a => t -> t -> a
foo _ _ = 0and then LiquidHaskell seems to ignore refts on (->), as that passes on its own.
A separate issue pops up if I leave off foo :: Num a => t -> t -> a. liquidhaskell complains that the LiquidHaskell type foo :: Num a => t -> t -> a does not match the inferred Haskell type foo :: Num a => t -> t -> a—so the type is not equal to itself.
|
For module Goo where
{-@ foo :: xs:_ -> {v:_ | this = rubbish } @-}
foo _ _ = 0into module Goo where
{-@ foo :: Num a => xs:t -> {v:(t -> a) | this = rubbish } @-}
foo :: Num a => t -> t -> a
foo _ _ = 0and then LiquidHaskell seems to ignore refts on A separate issue pops up if I leave off |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 27, 2015
Member
badspec{1,2}.hs come from a different problem: GHC's expandTypeSynonyms doesn't raise an error if a type synonym has invalid arguments (as it's just Type -> Type, no monad). This why the issue only occurs for Haskell type synonyms and not LiquidHaskell type synonyms:
module Zoo where
type Foo = Int
{-@ type Fooz X = {v:Int | X < v} @-}
{-@ bob :: Foo 1000 @-}
bob = 10 :: Intwhich is "SAFE", vs.
module Zoo where
type Foo = Int
{-@ type Fooz = {v:Int | 1 < v} @-}
{-@ bob :: Fooz 1000 @-}
bob = 10 :: Intwhich produces a LiquidHaskell error.
There must be a function somewhere in the GHC API that can raise these errors for us. I'd rather track one down and use that than have us implement these checks ourselves...
|
module Zoo where
type Foo = Int
{-@ type Fooz X = {v:Int | X < v} @-}
{-@ bob :: Foo 1000 @-}
bob = 10 :: Intwhich is "SAFE", vs. module Zoo where
type Foo = Int
{-@ type Fooz = {v:Int | 1 < v} @-}
{-@ bob :: Fooz 1000 @-}
bob = 10 :: Intwhich produces a LiquidHaskell error. There must be a function somewhere in the GHC API that can raise these errors for us. I'd rather track one down and use that than have us implement these checks ourselves... |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 27, 2015
Member
The relevant GHC code for that is here: https://github.com/ghc/ghc/blob/ghc-7.8/compiler/types/TyCon.lhs#L1427
GHC silently discards (doesn't expand) type synonyms with too many arguments. Odd behavior, but I'm sure there's a reason for it within GHC.
|
The relevant GHC code for that is here: https://github.com/ghc/ghc/blob/ghc-7.8/compiler/types/TyCon.lhs#L1427 GHC silently discards (doesn't expand) type synonyms with too many arguments. Odd behavior, but I'm sure there's a reason for it within GHC. |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
ranjitjhala
Mar 27, 2015
Member
Sorry I don't quite understand. Does it complain now or not?
On Fri, Mar 27, 2015 at 4:37 PM, Michael Smith notifications@github.com
wrote:
For badspec.hs, plugHoles turns
module Goo where
{-@ foo :: xs:_ -> {v:_ | this = rubbish } @-}
foo _ _ = 0into
module Goo where
{-@ foo :: Num a => xs:t -> {v:(t -> a) | this = rubbish } @-}foo :: Num a => t -> t -> a
foo _ _ = 0and then LiquidHaskell seems to ignore refts on (->), as that passes on
its own.A separate issue pops up if I leave off foo :: Num a => t -> t -> a.
liquidhaskell complains that the LiquidHaskell type foo :: Num a => t ->
t -> a does not match the inferred Haskell type foo :: Num a => t -> t ->
a--so the type is not equal to itself.Reply to this email directly or view it on GitHub
#292 (comment)
.
Ranjit.
|
Sorry I don't quite understand. Does it complain now or not? On Fri, Mar 27, 2015 at 4:37 PM, Michael Smith notifications@github.com
Ranjit. |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 28, 2015
Member
Breaking it down:
-
badspec.hs: LiquidHaskell ignores all predicates on(->), sothis == rubbishisn't checked or used at all as the hole gets filled with(t -> a). It doesn't complain on the test case (when it should), but it does complain onmodule Goo where {-@ foo :: xs:_ -> {v:_ | this = rubbish } @-} foo _ = 0
in which case
v:_becomesv:a. -
badspec{1,2}.hs: We useexpandTypeSynonymsto handle Haskell type synonym expansion, but this silently passes through cases where a type synonym is applied to too many arguments. LiquidHaskell should complain here, but it doesn't. It does complain (as it should) when we're using a LiquidHaskell synonym (like{-@ type Nat = {v:Int | 0 <= v} @-}), as we do our own checks in that case.
|
Breaking it down:
|
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 28, 2015
Member
I'm currently trying to find a GHC function to do these sanity checks on Types (for badspec{1,2}.hs). If anyone knows of one, please let me know! If I can't find one, I'll fall back to implementing one myself...
|
I'm currently trying to find a GHC function to do these sanity checks on |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
ranjitjhala
Mar 28, 2015
Member
Can we just compare the number of params with that expected by the synonym in ghc?
On Mar 27, 2015, at 5:02 PM, Michael Smith notifications@github.com wrote:
I'm currently trying to find a GHC function to do these sanity checks on Types. If anyone knows one, please let me know! If I can't find one, I'll fall back to implementing one myself...
—
Reply to this email directly or view it on GitHub.
|
Can we just compare the number of params with that expected by the synonym in ghc?
|
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 28, 2015
Member
Yes, but I'd like to use existing GHC mechanisms where we can... I think tcLHsType from TcHsType will do the job, but otherwise I'll just do that.
|
Yes, but I'd like to use existing GHC mechanisms where we can... I think |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 28, 2015
Member
Ah, tcLHsType can only be called from within TcM... Alright, I'll just add the check in myself and let this get sorted out by the GSoC work.
|
Ah, |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
gridaphobe
Mar 28, 2015
Contributor
(1) should be easy to fix, just throw an error if a function is refined with anything other than TRUE.
for (2), the issue may be that Haskell type synonyms can be eta reduced just like functions, e.g. a common pattern is
type MyMonad = State Foowhere the "result" type a is left out. Thus when GHC sees MyMonad Int it doesn't know immediately whether the type is well-formed (State could be another alias). The check might need to be deferred until the last moment.
|
(1) should be easy to fix, just throw an error if a function is refined with anything other than TRUE. for (2), the issue may be that Haskell type synonyms can be eta reduced just like functions, e.g. a common pattern is type MyMonad = State Foowhere the "result" type |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 28, 2015
Member
Ah, I see. That makes sense for (2), thanks. For (1), we don't support refinements on functions at all then, right?
|
Ah, I see. That makes sense for (2), thanks. For (1), we don't support refinements on functions at all then, right? |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
ranjitjhala
Mar 28, 2015
Member
I don't buy the argument re 2 -- in this case the parameter we are passing in is a binder n and not a type variable, so we cannot blame GHc
On Mar 27, 2015, at 5:30 PM, Michael Smith notifications@github.com wrote:
Ah, I see. That makes sense for (2), thanks. For (1), we don't support refinements on functions at all then, right?
—
Reply to this email directly or view it on GitHub.
|
I don't buy the argument re 2 -- in this case the parameter we are passing in is a binder n and not a type variable, so we cannot blame GHc
|
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
ranjitjhala
Mar 28, 2015
Member
Yes, I agree with Michael's plan
On Mar 27, 2015, at 5:14 PM, Michael Smith notifications@github.com wrote:
Yes, but I'd like to use existing GHC mechanisms where we can... I think tcLHsType will do the job, but otherwise I'll just do that.
—
Reply to this email directly or view it on GitHub.
|
Yes, I agree with Michael's plan
|
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
gridaphobe
Mar 28, 2015
Contributor
@ranjitjhala oh I agree completely that it's our fault, I was just giving a possible explanation for why expandTypeSynonyms doesn't throw any errors.
|
@ranjitjhala oh I agree completely that it's our fault, I was just giving a possible explanation for why |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 28, 2015
Member
@ranjitjhala, by "2" do you mean badspec2.hs? I meant to refer to both badspec{1,2}.hs there.
For badspec2.hs, Point is applied to too many type synonyms, and since expandTypeSynonyms doesn't check for that we need to add our own check.
If we remove this issue, then we do actually error out due to the overlapping binder and type variable names, but in a weird way:
module Foo where
type List a = [a]
type Point a = List a
{-@ foo :: n:Nat -> Point n @-}
foo :: Int -> List Double
foo _ = []LiquidHaskell Copyright 2009-14 Regents of the University of California. All Rights Reserved.
**** DONE: annotate ***********************************************************
**** ERROR: *******************************************************************
tests/crash/badspec2.hs:6:5: Error: Specified Type Does Not Refine Haskell Type for Foo.foo
Haskell: GHC.Types.Int -> [GHC.Types.Double]
Liquid : forall n. GHC.Types.Int -> [n]
Do we do any checks for this already?
|
@ranjitjhala, by "2" do you mean For If we remove this issue, then we do actually error out due to the overlapping binder and type variable names, but in a weird way: module Foo where
type List a = [a]
type Point a = List a
{-@ foo :: n:Nat -> Point n @-}
foo :: Int -> List Double
foo _ = []Do we do any checks for this already? |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
gridaphobe
Mar 28, 2015
Contributor
Hrm, I'm not sure what you did to "remove" the issue, but that error is completely wrong. There shouldn't be a forall in the liquid type.
|
Hrm, I'm not sure what you did to "remove" the issue, but that error is completely wrong. There shouldn't be a |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
ranjitjhala
Mar 28, 2015
Member
The "n" has nothing to do with expand type synonym thing here, because the n is a binder NOT a haskell tyvar it should not even go to ghc...
On Mar 27, 2015, at 5:56 PM, Eric Seidel notifications@github.com wrote:
Hrm, I'm not sure what you did to "remove" the issue, but that error is completely wrong. There shouldn't be a forall in the liquid type.
—
Reply to this email directly or view it on GitHub.
|
The "n" has nothing to do with expand type synonym thing here, because the n is a binder NOT a haskell tyvar it should not even go to ghc...
|
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 28, 2015
Member
"remove" the too-many-arguments issue by adding a parameter to Point, isolating the "binder as type variable" problem.
That error message is actually because I left in the old explicit signature for foo... If I change it, we get:
module Foo where
type List a = [a]
type Point a = List a
{-@ foo :: n:Nat -> Point n @-}
foo :: Int -> List n
foo _ = []LiquidHaskell Copyright 2009-14 Regents of the University of California. All Rights Reserved.
**** DONE: Extracted Core using GHC *******************************************
**** DONE: generateConstraints ************************************************
**** START: fixpoint ***********************************************************
========================================================
© Copyright 2009 Regents of the University of California.
All Rights Reserved.
========================================================
.|
SAT
**** DONE: fixpoint ***********************************************************
**** DONE: solve **************************************************************
**** DONE: annotate ***********************************************************
**** SAFE **********************************************************************
I'm not sure what the correct way to handle this is. The current behavior (if I understand correctly) is for type variables to exist in their own namespace, and overlapping with binder names is allowed. Should we forbid this?
|
"remove" the too-many-arguments issue by adding a parameter to That error message is actually because I left in the old explicit signature for module Foo where
type List a = [a]
type Point a = List a
{-@ foo :: n:Nat -> Point n @-}
foo :: Int -> List n
foo _ = []I'm not sure what the correct way to handle this is. The current behavior (if I understand correctly) is for type variables to exist in their own namespace, and overlapping with binder names is allowed. Should we forbid this? |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 28, 2015
Member
@ranjitjhala, it does in the original test case:
module Foo where
type List a = [a]
type Point = List Double
{-@ foo :: n:Nat -> Point n @-}
foo :: Int -> List Double
foo _ = []which combined two separate issues: allowing "Point" to be applied to too many type arguments, and using a binder as a type variable. Sorry for not being clear here.
|
@ranjitjhala, it does in the original test case: module Foo where
type List a = [a]
type Point = List Double
{-@ foo :: n:Nat -> Point n @-}
foo :: Int -> List Double
foo _ = []which combined two separate issues: allowing "Point" to be applied to too many type arguments, and using a binder as a type variable. Sorry for not being clear here. |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
ranjitjhala
Mar 28, 2015
Member
I have no idea what's going on :)
Bottom line : "n" is not something we can ask ghc to expand because it's a binder and that is a bug that we should catch.
On Mar 27, 2015, at 6:07 PM, Michael Smith notifications@github.com wrote:
@ranjitjhala, it does in the original test case:
module Foo where
type List a = [a]
type Point = List Double{-@ foo :: n:Nat -> Point n @-}
foo :: Int -> List Double
foo _ = []
which combined two separate issues: allowing "Point" to be applied to too many type arguments, and using a binder as a type variable.—
Reply to this email directly or view it on GitHub.
|
I have no idea what's going on :) Bottom line : "n" is not something we can ask ghc to expand because it's a binder and that is a bug that we should catch.
|
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
ranjitjhala
Mar 28, 2015
Member
The current behavior (if I understand correctly) is for type variables to exist in their own namespace, and overlapping with binder names is allowed. Should we forbid this?
Absolutely this should be completely disallowed it makes no sense!
Absolutely this should be completely disallowed it makes no sense! |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
ranjitjhala
Mar 28, 2015
Member
This overlapping is exactly the cause of the bug yeah, we should check for it and project such programs.
On Mar 27, 2015, at 6:14 PM, Ranjit Jhala rjhala@eng.ucsd.edu wrote:
The current behavior (if I understand correctly) is for type variables to exist in their own namespace, and overlapping with binder names is allowed. Should we forbid this?
Absolutely this should be completely disallowed it makes no sense!
|
This overlapping is exactly the cause of the bug yeah, we should check for it and project such programs.
|
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 28, 2015
Member
Right, okay, sorry. :) Let me make sure I have everything straight now:
So currently we (accidentally) treat binders and type variables like GHC treats type constructors and data constructors: they exist in different namespaces and their names can overlap. There's no ambiguous case (I think) where something can either be a binder or a type variable.
The signature
{-@ foo :: n:Nat -> Point n @-}is equivalent to
{-@ foo :: forall n. n:Nat -> Point n @-}is equivalent to
{-@ foo :: forall n0. n1:Nat -> Point n0 @-}because Point n must always be referring to the type variable n, not the binder n.
Instead, we want to add a check for this case and reject programs that use this, because this is confusing behavior. I can do that!
|
Right, okay, sorry. :) Let me make sure I have everything straight now: So currently we (accidentally) treat binders and type variables like GHC treats type constructors and data constructors: they exist in different namespaces and their names can overlap. There's no ambiguous case (I think) where something can either be a binder or a type variable. The signature {-@ foo :: n:Nat -> Point n @-}is equivalent to {-@ foo :: forall n. n:Nat -> Point n @-}is equivalent to {-@ foo :: forall n0. n1:Nat -> Point n0 @-}because Instead, we want to add a check for this case and reject programs that use this, because this is confusing behavior. I can do that! |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
gridaphobe
Mar 28, 2015
Contributor
It might be easiest to separate binders and tyvars immediately after parsing. Then
{-@ foo :: n:Nat -> Point n @-}
would treat both occurences of n as binders, and throw an error when we apply the Haskell alias Point to the binder n.
|
It might be easiest to separate binders and tyvars immediately after parsing. Then would treat both occurences of |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 28, 2015
Member
Working on badspec.hs, is there a reason why RFun has an rt_reft field at all? Is it used anywhere, or can it be taken out? It seems to always be TRUE.
|
Working on |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
ranjitjhala
Mar 28, 2015
Member
It's there for some very technical but important reasons -- can you keep it in? We always want to make sure it's just true ie "top"
On Mar 27, 2015, at 6:48 PM, Michael Smith notifications@github.com wrote:
Working on badspec.hs, is there a reason why RFun has an rt_reft field at all? Is it used anywhere, or can it be taken out?
—
Reply to this email directly or view it on GitHub.
|
It's there for some very technical but important reasons -- can you keep it in? We always want to make sure it's just true ie "top"
|
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 28, 2015
Member
Sure, I can keep it in. Somewhere between makePluggedSigs and checkRType, rt_reft for all RFun is being set to TRUE. Going to track that down next.
|
Sure, I can keep it in. Somewhere between |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 28, 2015
Member
The refinements for RFun were being lost between translations to and from RTypeRep. I've fixed this by storing them in RTypeRep in the same way that we store binders.
|
The refinements for |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
nikivazou
Mar 28, 2015
Member
No need to store them. The refinements on functions are always true.
On Mar 28, 2015 12:28 AM, "Michael Smith" notifications@github.com wrote:
The refinements for RFun were being lost between translations to and from
RTypeRep. I've fixed this by storing them in RTypeRep in the same way
that we store binders.—
Reply to this email directly or view it on GitHub
#292 (comment)
.
|
No need to store them. The refinements on functions are always true.
|
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 28, 2015
Member
We need to store them in order to report errors if any of them are not true.
On Sat, Mar 28, 2015, 16:04 Niki Vazou notifications@github.com wrote:
No need to store them. The refinements on functions are always true.
On Mar 28, 2015 12:28 AM, "Michael Smith" notifications@github.com
wrote:The refinements for RFun were being lost between translations to and from
RTypeRep. I've fixed this by storing them in RTypeRep in the same way
that we store binders.—
Reply to this email directly or view it on GitHub
<
#292 (comment).
—
Reply to this email directly or view it on GitHub
#292 (comment)
.
|
We need to store them in order to report errors if any of them are not true. On Sat, Mar 28, 2015, 16:04 Niki Vazou notifications@github.com wrote:
|
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
ranjitjhala
Mar 28, 2015
Member
But remember that soundness issue involving instantiating tyvarS (with refinements) with functions (without refinements)...
On Mar 28, 2015, at 4:05 PM, Michael Smith notifications@github.com wrote:
We need to store them in order to report errors if any of them are not true.
On Sat, Mar 28, 2015, 16:04 Niki Vazou notifications@github.com wrote:
No need to store them. The refinements on functions are always true.
On Mar 28, 2015 12:28 AM, "Michael Smith" notifications@github.com
wrote:The refinements for RFun were being lost between translations to and from
RTypeRep. I've fixed this by storing them in RTypeRep in the same way
that we store binders.—
Reply to this email directly or view it on GitHub
<
#292 (comment).
—
Reply to this email directly or view it on GitHub
#292 (comment)
.—
Reply to this email directly or view it on GitHub.
|
But remember that soundness issue involving instantiating tyvarS (with refinements) with functions (without refinements)...
|
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
nikivazou
Mar 28, 2015
Member
Yes this is why we added refinements to functions. But they are always
true, right?
On Mar 28, 2015 4:10 PM, "Ranjit Jhala" notifications@github.com wrote:
But remember that soundness issue involving instantiating tyvarS (with
refinements) with functions (without refinements)...On Mar 28, 2015, at 4:05 PM, Michael Smith notifications@github.com
wrote:We need to store them in order to report errors if any of them are not
true.On Sat, Mar 28, 2015, 16:04 Niki Vazou notifications@github.com wrote:
No need to store them. The refinements on functions are always true.
On Mar 28, 2015 12:28 AM, "Michael Smith" notifications@github.com
wrote:The refinements for RFun were being lost between translations to and
from
RTypeRep. I've fixed this by storing them in RTypeRep in the same way
that we store binders.—
Reply to this email directly or view it on GitHub
<.
—
Reply to this email directly or view it on GitHub
<
#292 (comment).
—
Reply to this email directly or view it on GitHub.—
Reply to this email directly or view it on GitHub
#292 (comment)
.
|
Yes this is why we added refinements to functions. But they are always
|
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 28, 2015
Member
Right now a user can specify a refinement on a function type, and it will
be silently discarded and replaced with true by the end of the Bare
processing. This is why badspec.hs is marked as "SAFE", which I'm fixing
with this.
On Sat, Mar 28, 2015, 16:13 Niki Vazou notifications@github.com wrote:
Yes this is why we added refinements to functions. But they are always
true, right?
On Mar 28, 2015 4:10 PM, "Ranjit Jhala" notifications@github.com wrote:But remember that soundness issue involving instantiating tyvarS (with
refinements) with functions (without refinements)...On Mar 28, 2015, at 4:05 PM, Michael Smith notifications@github.com
wrote:We need to store them in order to report errors if any of them are not
true.On Sat, Mar 28, 2015, 16:04 Niki Vazou notifications@github.com
wrote:No need to store them. The refinements on functions are always true.
On Mar 28, 2015 12:28 AM, "Michael Smith" notifications@github.com
wrote:The refinements for RFun were being lost between translations to
and
from
RTypeRep. I've fixed this by storing them in RTypeRep in the same
way
that we store binders.—
Reply to this email directly or view it on GitHub
<.
—
Reply to this email directly or view it on GitHub
<.
—
Reply to this email directly or view it on GitHub.—
Reply to this email directly or view it on GitHub
<
#292 (comment).
—
Reply to this email directly or view it on GitHub
#292 (comment)
.
|
Right now a user can specify a refinement on a function type, and it will On Sat, Mar 28, 2015, 16:13 Niki Vazou notifications@github.com wrote:
|
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
ranjitjhala
Mar 28, 2015
Member
Yup!
On Mar 28, 2015, at 4:13 PM, Niki Vazou notifications@github.com wrote:
Yes this is why we added refinements to functions. But they are always
true, right?
On Mar 28, 2015 4:10 PM, "Ranjit Jhala" notifications@github.com wrote:But remember that soundness issue involving instantiating tyvarS (with
refinements) with functions (without refinements)...On Mar 28, 2015, at 4:05 PM, Michael Smith notifications@github.com
wrote:We need to store them in order to report errors if any of them are not
true.On Sat, Mar 28, 2015, 16:04 Niki Vazou notifications@github.com wrote:
No need to store them. The refinements on functions are always true.
On Mar 28, 2015 12:28 AM, "Michael Smith" notifications@github.com
wrote:The refinements for RFun were being lost between translations to and
from
RTypeRep. I've fixed this by storing them in RTypeRep in the same way
that we store binders.—
Reply to this email directly or view it on GitHub
<.
—
Reply to this email directly or view it on GitHub
<
#292 (comment).
—
Reply to this email directly or view it on GitHub.—
Reply to this email directly or view it on GitHub
#292 (comment)
.—
Reply to this email directly or view it on GitHub.
|
Yup!
|
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 28, 2015
Member
They should always be true, but they can end up not being true, and we
need to handle that instead of ignoring bad refinements.
On Sat, Mar 28, 2015, 16:16 Ranjit Jhala notifications@github.com wrote:
Yup!
On Mar 28, 2015, at 4:13 PM, Niki Vazou notifications@github.com
wrote:Yes this is why we added refinements to functions. But they are always
true, right?
On Mar 28, 2015 4:10 PM, "Ranjit Jhala" notifications@github.com
wrote:But remember that soundness issue involving instantiating tyvarS (with
refinements) with functions (without refinements)...On Mar 28, 2015, at 4:05 PM, Michael Smith <notifications@github.com
wrote:
We need to store them in order to report errors if any of them are
not
true.On Sat, Mar 28, 2015, 16:04 Niki Vazou notifications@github.com
wrote:No need to store them. The refinements on functions are always
true.
On Mar 28, 2015 12:28 AM, "Michael Smith" <
notifications@github.com>
wrote:The refinements for RFun were being lost between translations to
and
from
RTypeRep. I've fixed this by storing them in RTypeRep in the
same way
that we store binders.—
Reply to this email directly or view it on GitHub
<.
—
Reply to this email directly or view it on GitHub
<.
—
Reply to this email directly or view it on GitHub.—
Reply to this email directly or view it on GitHub
<
#292 (comment).
—
Reply to this email directly or view it on GitHub.—
Reply to this email directly or view it on GitHub
#292 (comment)
.
|
They should always be true, but they can end up not being true, and we On Sat, Mar 28, 2015, 16:16 Ranjit Jhala notifications@github.com wrote:
|
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
nikivazou
Mar 28, 2015
Member
I see.
But then, the parser should reject refining function type.
On Mar 28, 2015 4:21 PM, "Michael Smith" notifications@github.com wrote:
They should always be true, but they can end up not being true, and we
need to handle that instead of ignoring bad refinements.On Sat, Mar 28, 2015, 16:16 Ranjit Jhala notifications@github.com wrote:
Yup!
On Mar 28, 2015, at 4:13 PM, Niki Vazou notifications@github.com
wrote:Yes this is why we added refinements to functions. But they are always
true, right?
On Mar 28, 2015 4:10 PM, "Ranjit Jhala" notifications@github.com
wrote:But remember that soundness issue involving instantiating tyvarS
(with
refinements) with functions (without refinements)...On Mar 28, 2015, at 4:05 PM, Michael Smith <
notifications@github.comwrote:
We need to store them in order to report errors if any of them are
not
true.On Sat, Mar 28, 2015, 16:04 Niki Vazou notifications@github.com
wrote:No need to store them. The refinements on functions are always
true.
On Mar 28, 2015 12:28 AM, "Michael Smith" <
notifications@github.com>
wrote:The refinements for RFun were being lost between translations
to
and
from
RTypeRep. I've fixed this by storing them in RTypeRep in the
same way
that we store binders.—
Reply to this email directly or view it on GitHub
<.
—
Reply to this email directly or view it on GitHub
<.
—
Reply to this email directly or view it on GitHub.—
Reply to this email directly or view it on GitHub
<.
—
Reply to this email directly or view it on GitHub.—
Reply to this email directly or view it on GitHub
<
#292 (comment).
—
Reply to this email directly or view it on GitHub
#292 (comment)
.
|
I see.
|
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 28, 2015
Member
The function type can have a refinement attached to it after parsing, through
type synonym expansion or through plugHoles (as in badspec.hs). Also,
reporting it as a parse error means the user sees fewer possible errors per
LiquidHaskell run, vs. reporting it in checkGhcSpec.
On Sat, Mar 28, 2015, 16:26 Niki Vazou notifications@github.com wrote:
I see.
But then, the parser should reject refining function type.
On Mar 28, 2015 4:21 PM, "Michael Smith" notifications@github.com wrote:They should always be true, but they can end up not being true, and we
need to handle that instead of ignoring bad refinements.On Sat, Mar 28, 2015, 16:16 Ranjit Jhala notifications@github.com
wrote:Yup!
On Mar 28, 2015, at 4:13 PM, Niki Vazou notifications@github.com
wrote:Yes this is why we added refinements to functions. But they are
always
true, right?
On Mar 28, 2015 4:10 PM, "Ranjit Jhala" notifications@github.com
wrote:But remember that soundness issue involving instantiating tyvarS
(with
refinements) with functions (without refinements)...On Mar 28, 2015, at 4:05 PM, Michael Smith <
notifications@github.comwrote:
We need to store them in order to report errors if any of them
are
not
true.On Sat, Mar 28, 2015, 16:04 Niki Vazou <notifications@github.com
wrote:
No need to store them. The refinements on functions are always
true.
On Mar 28, 2015 12:28 AM, "Michael Smith" <
notifications@github.com>
wrote:The refinements for RFun were being lost between translations
to
and
from
RTypeRep. I've fixed this by storing them in RTypeRep in the
same way
that we store binders.—
Reply to this email directly or view it on GitHub
<.
—
Reply to this email directly or view it on GitHub
<.
—
Reply to this email directly or view it on GitHub.—
Reply to this email directly or view it on GitHub
<.
—
Reply to this email directly or view it on GitHub.—
Reply to this email directly or view it on GitHub
<.
—
Reply to this email directly or view it on GitHub
<
#292 (comment).
—
Reply to this email directly or view it on GitHub
#292 (comment)
.
|
The function type can have a refinement attached to it after parsing, through On Sat, Mar 28, 2015, 16:26 Niki Vazou notifications@github.com wrote:
|
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
nikivazou
Mar 28, 2015
Member
As Ranjit says for soundness function types should have refinements.
What I am saying is that since the user cannot specify non trivial function
refinements the syntax should not allow refinements on functions.
I believe this is simpler than specifying that the syntax allows these
refinements, but they should be true.
If the syntax does not allow refinements on functions and the user writes
them then we have a parsing error, and the program fails without analyzing
the rest of your code, as GHC does.
On Mar 28, 2015 4:28 PM, "Michael Smith" notifications@github.com wrote:
The function type have a refinement attached to it after parsing, through
type synonym expansion or through plugHoles (as in badspec.hs). Also,
reporting it as a parser means the user sees fewer possible errors per
LiquidHaskell run, vs. reporting it in checkGhcSpec.On Sat, Mar 28, 2015, 16:26 Niki Vazou notifications@github.com wrote:
I see.
But then, the parser should reject refining function type.
On Mar 28, 2015 4:21 PM, "Michael Smith" notifications@github.com
wrote:They should always be true, but they can end up not being true, and
we
need to handle that instead of ignoring bad refinements.On Sat, Mar 28, 2015, 16:16 Ranjit Jhala notifications@github.com
wrote:Yup!
On Mar 28, 2015, at 4:13 PM, Niki Vazou notifications@github.com
wrote:Yes this is why we added refinements to functions. But they are
always
true, right?
On Mar 28, 2015 4:10 PM, "Ranjit Jhala" notifications@github.com
wrote:But remember that soundness issue involving instantiating tyvarS
(with
refinements) with functions (without refinements)...On Mar 28, 2015, at 4:05 PM, Michael Smith <
notifications@github.comwrote:
We need to store them in order to report errors if any of them
are
not
true.On Sat, Mar 28, 2015, 16:04 Niki Vazou <
notifications@github.comwrote:
No need to store them. The refinements on functions are
always
true.
On Mar 28, 2015 12:28 AM, "Michael Smith" <
notifications@github.com>
wrote:The refinements for RFun were being lost between
translations
to
and
from
RTypeRep. I've fixed this by storing them in RTypeRep in
the
same way
that we store binders.—
Reply to this email directly or view it on GitHub
<.
—
Reply to this email directly or view it on GitHub
<.
—
Reply to this email directly or view it on GitHub.—
Reply to this email directly or view it on GitHub
<.
—
Reply to this email directly or view it on GitHub.—
Reply to this email directly or view it on GitHub
<.
—
Reply to this email directly or view it on GitHub
<.
—
Reply to this email directly or view it on GitHub
<
#292 (comment).
—
Reply to this email directly or view it on GitHub
#292 (comment)
.
|
As Ranjit says for soundness function types should have refinements. What I am saying is that since the user cannot specify non trivial function If the syntax does not allow refinements on functions and the user writes
|
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 28, 2015
Member
That doesn't help with the original issue, though (badspec.hs). An invalid
refinement is assigned to a function type via plugHoles, and by discarding
the refinement instead of passing it through (to either check or Fixpoint),
we mark a malformed spec as "SAFE".
GHC actually allows some things through the parsing stage so that it can
report more errors at once, and to avoid overcomplicating the parsing code.
But we could make this a parse error or something, in addition to passing
refinements all the way through, if we only want to eliminate explicit
refinements on functions. That would create an inconcistency when using
plugHoles, though.
On Sat, Mar 28, 2015, 16:38 Niki Vazou notifications@github.com wrote:
As Ranjit says for soundness function types should have refinements.
What I am saying is that since the user cannot specify non trivial function
refinements the syntax should not allow refinements on functions.
I believe this is simpler than specifying that the syntax allows these
refinements, but they should be true.If the syntax does not allow refinements on functions and the user writes
them then we have a parsing error, and the program fails without analyzing
the rest of your code, as GHC does.
On Mar 28, 2015 4:28 PM, "Michael Smith" notifications@github.com wrote:The function type have a refinement attached to it after parsing, through
type synonym expansion or through plugHoles (as in badspec.hs). Also,
reporting it as a parser means the user sees fewer possible errors per
LiquidHaskell run, vs. reporting it in checkGhcSpec.On Sat, Mar 28, 2015, 16:26 Niki Vazou notifications@github.com wrote:
I see.
But then, the parser should reject refining function type.
On Mar 28, 2015 4:21 PM, "Michael Smith" notifications@github.com
wrote:They should always be true, but they can end up not being true, and
we
need to handle that instead of ignoring bad refinements.On Sat, Mar 28, 2015, 16:16 Ranjit Jhala notifications@github.com
wrote:Yup!
On Mar 28, 2015, at 4:13 PM, Niki Vazou <
notifications@github.com>
wrote:Yes this is why we added refinements to functions. But they are
always
true, right?
On Mar 28, 2015 4:10 PM, "Ranjit Jhala" <
notifications@github.com>
wrote:But remember that soundness issue involving instantiating
tyvarS
(with
refinements) with functions (without refinements)...On Mar 28, 2015, at 4:05 PM, Michael Smith <
notifications@github.comwrote:
We need to store them in order to report errors if any of
them
are
not
true.On Sat, Mar 28, 2015, 16:04 Niki Vazou <
notifications@github.comwrote:
No need to store them. The refinements on functions are
always
true.
On Mar 28, 2015 12:28 AM, "Michael Smith" <
notifications@github.com>
wrote:The refinements for RFun were being lost between
translations
to
and
from
RTypeRep. I've fixed this by storing them in RTypeRep in
the
same way
that we store binders.—
Reply to this email directly or view it on GitHub
<.
—
Reply to this email directly or view it on GitHub
<.
—
Reply to this email directly or view it on GitHub.—
Reply to this email directly or view it on GitHub
<.
—
Reply to this email directly or view it on GitHub.—
Reply to this email directly or view it on GitHub
<.
—
Reply to this email directly or view it on GitHub
<.
—
Reply to this email directly or view it on GitHub
<.
—
Reply to this email directly or view it on GitHub
<
#292 (comment).
—
Reply to this email directly or view it on GitHub
#292 (comment)
.
|
That doesn't help with the original issue, though (badspec.hs). An invalid GHC actually allows some things through the parsing stage so that it can On Sat, Mar 28, 2015, 16:38 Niki Vazou notifications@github.com wrote:
|
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
gridaphobe
Mar 28, 2015
Contributor
@nikivazou the parser already forbids writing types like {v:(a -> b) | p}, the problem is that you can instead write {v:_ | p} and have the hole instantiated to a function type, which the parser cannot prevent.
|
@nikivazou the parser already forbids writing types like |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 28, 2015
Member
@gridaphobe actually the parser doesn't forbid that currently.
module Goo where
{-@ foo :: Num a => xs:t -> {v:(t -> a) | this = rubbish } @-}
foo :: Num a => t -> t -> a
foo _ _ = 0LiquidHaskell Copyright 2009-14 Regents of the University of California. All Rights Reserved.
**** DONE: Extracted Core using GHC *******************************************
**** DONE: generateConstraints ************************************************
**** START: fixpoint ***********************************************************
========================================================
© Copyright 2009 Regents of the University of California.
All Rights Reserved.
========================================================
.|
SAT
**** DONE: fixpoint ***********************************************************
**** DONE: solve **************************************************************
**** DONE: annotate ***********************************************************
**** SAFE **********************************************************************
|
@gridaphobe actually the parser doesn't forbid that currently. module Goo where
{-@ foo :: Num a => xs:t -> {v:(t -> a) | this = rubbish } @-}
foo :: Num a => t -> t -> a
foo _ _ = 0 |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 28, 2015
Member
@gridaphobe But yes, that's exactly the problem with only checking it in the parser.
|
@gridaphobe But yes, that's exactly the problem with only checking it in the parser. |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
gridaphobe
Mar 28, 2015
Contributor
Well that's what I get for trying to read the parser code instead of just running an example.. In that case, I don't see a reason to tweak the parser, better to catch it in Bare along with all the other errors we look for.
|
Well that's what I get for trying to read the parser code instead of just running an example.. In that case, I don't see a reason to tweak the parser, better to catch it in Bare along with all the other errors we look for. |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
Mar 28, 2015
Member
And that's what I have implemented right now. I've modified the code to pass through refinements on function types all the way through the Bare pipeline, and then I added a check to checkGhcSpec to report errors. I should have it up in a PR soon-ish.
|
And that's what I have implemented right now. I've modified the code to pass through refinements on function types all the way through the Bare pipeline, and then I added a check to checkGhcSpec to report errors. I should have it up in a PR soon-ish. |
This was referenced Apr 1, 2015
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
|
@spinda, you fixed this, right? |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
spinda
closed this
Apr 17, 2015
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
nikivazou
Apr 17, 2015
Member
Thanks!
On Fri, Apr 17, 2015 at 3:45 PM, Michael Smith notifications@github.com
wrote:
—
Reply to this email directly or view it on GitHub
#292 (comment)
.
Niki Vazou
|
Thanks! On Fri, Apr 17, 2015 at 3:45 PM, Michael Smith notifications@github.com
Niki Vazou |
This comment has been minimized.
Show comment
Hide comment
This comment has been minimized.
ranjitjhala
Apr 18, 2015
Member
Thanks!!
On Apr 18, 2015, at 4:15 AM, Michael Smith notifications@github.com wrote:
Closed #292.
—
Reply to this email directly or view it on GitHub.
|
Thanks!!
|
ranjitjhala commentedJan 1, 2015
See https://github.com/ucsd-progsys/liquidhaskell/blob/master/tests/todo/badspec.hs
See https://github.com/ucsd-progsys/liquidhaskell/blob/master/tests/todo/badspec1.hs
This should be rejected...