Advice for #11475

[Richard Eisenberg]

Hi Jonas,

Thanks for jumping in! It sounds like you're very much on the right track here, and I appreciate your desire not to use the simplifier code in the linter.

I'm afraid I don't have good answers for your questions, however. Really, this email is just to offer some gratitude and hope you can wait for someone more knowledgeable about the simplifier (e.g., SPJ) to answer.

I have to say that I'm worried here that the Right Answer will involve having the simplifier produce some evidence for its pruning ideas, so that the linter can simply verify the evidence. This evidence would be in the form of a small data structure with constructors that say "looked through identifier <<id>>" or "scrutinee is a constructor call of <<ctor>>" or similar. Then the linter's job is made much easier.

Richard

On Feb 19, 2016, at 6:13 AM, Jonas Scholl <anselm.scholl at tu-harburg.de> wrote:

> Hello GHC-Devs,
> 
> I am currently giving #11475 a try. However I hit a few problems and
> wanted to ask for a bit of advice about how to proceed.
> 
> I already can handle the following:
> 
> case x of
>  A y -> e1
>  _   -> ....(case x of
>                B -> r2
>                C -> r3) ...
> 
> My first problem then was the following construct:
> 
> case (case ... of ... -> Left x) of
>  Left y -> ...
> 
> Or more simple:
> 
> case Left x of
>  Left y -> ...
> 
> So I have to check which constructors the scrutinee may return. I know
> the simplifier has to implement such logic somewhere but did not want to
> use the implementation for two reasons:
> - I didn't know where to find it
> - If GHC uses the same test to prune impossible alternatives and to
> check if they were pruned correctly, extending the linter is useless. A
> bug in the test code will cause also cause a bug in the linter.
> 
> So I implemented such a test myself, but now I am stuck at something
> like this:
> 
> foo a b = a : b
> 
> bar = ... case foo a b of
>  (:) x y -> ...
> 
> I cannot see through foo, so I assume it may return (:) and []. The
> simplifier on the other hand is able to see through foo and did remove
> the [] case, causing my current implementation to throw an incorrect
> lint error.
> 
> How can I get a list/set of all possible AltCons returned by a
> function/constant? Or a list of the impossible ones? I tried to get some
> information from the unfolding of a variable, but it seems like
> unfoldings are only attached to top-level names.
> 
> Jonas
> 
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs