Opened 11 months ago

Closed 7 months ago

#14691 closed task (fixed)

Replace EvTerm with CoreExpr

Reported by: nomeata Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.3
Keywords: TypeCheckerPlugins Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

I asked

I had some funky idea where a type checker plugin would have to | synthesize code for a custom-solved instances on the fly. But it seems that does not work because EvTerm is less expressive than Core (especially, no lambdas)

What would break if we had

 | EvExpr CoreExpr

as an additional constructor there?

And Simon said

This has come up before. I think that'd be a solid win.

In fact, eliminate all the existing evidence constructors with "smart constructors" that produce an EvExpr. That'd mean moving stuff from the desugarer into these smart constructors, but that's ok.

I /think/ I didn't do that initially only because there were very few forms and it mean that there was no CoreExpr stuff in the type checker. But as we add more forms that decision looks and less good.

You'd need to add zonkCoreExpr in place of zonkEvTerm.

evVarsOfTerm is called quite a bit; you might want to cache the result in the EvExpr constructor.

This ticket tracks it. Not sure if i get to it right away, but I am happy to advise, review, and play around with the result.

Change History (29)

comment:1 Changed 11 months ago by nomeata

Is it correct that the evVarsOfTerm are those free variables of the expression for which isEvVar is true, i.e.

evVarsOfTerm evExpr = filter isEvVar (exprFreeVars (dsEvTerm evExpr))

comment:2 Changed 11 months ago by nomeata

evVarsOfTerm is called quite a bit; you might want to cache the result in the EvExpr constructor.

evVarsOfTerm is not cached at the moment. Do you think that exprSomeFreeVars isEvVar is going to be significantly slower?

comment:3 Changed 11 months ago by nomeata

Prelimary work in wip/14691.

But here is slight refactoring annoyance: The code from dsEvTerm would have to move into the new smart constructors, e.g. evTypeable, which replaces EvTypable. But the former is monadic (in DsM, to lookup things), while the latter is pure. So the uses of these smart constructors need to be made monadic. It seems to affect evTypeable, evCallStack and evLit, it looks like the other smart constructors can remain pure.

comment:4 Changed 11 months ago by nomeata

When moving this desugaring code into smart constructors that are run by the type checker, it need to be able ot use functions like mkStringExprFS which require MonadThings. But the type checker monad does not have a suitable instance:

No instance for (HscTypes.MonadThings TcS)

Is that by design, or has just nobody bothered so far to create such an instance?

I assume the latter, and added an instance now.

Last edited 11 months ago by nomeata (previous) (diff)

comment:5 Changed 11 months ago by nomeata

When zonking a CoreExpr, is there a need to zonk inside a Tickish?

comment:6 Changed 11 months ago by nomeata

Ok, wip/14691 has a complete refactoring. Time to address the fallout, and advise is welcome…

I get

libraries/base/Data/Typeable/Internal.hs:1:1: error:
    GHC internal error: ‘mkTrCon’ is not in scope during type checking, but it passed the renamer

It seems that this code:

ds_ev_typeable :: MonadThings m => Type -> EvTypeable -> m CoreExpr
ds_ev_typeable ty (EvTypeableTyCon tc kind_ev)
  = do { mkTrCon <- lookupId mkTrConName
…

does not quite work when the current module is Data.Typeable.Internal, which is where mkTrCon is defined. Do I need a smarter lookupId that checks if the given name is supposed to be defined in the current module, and then uses the local name, rather than trying to find the global name?

comment:7 Changed 11 months ago by nomeata

Do I need a smarter lookupId that checks if the given name is supposed to be defined in the current module, and then uses the local name, rather than trying to find the global name?

It seems that lookupId (which is tcLookupGlobal) already does that. But maybe the local definitions are not in the environment properly at the time TcInteract does its work?

comment:8 Changed 11 months ago by simonpj

‘mkTrCon’ is not in scope during type checking,

Well that's very tiresome. mkTrCon

  • is defined in Data.Typeable.Internal
  • is used when generating Typeable evidence

But it's not in the environment early enough.

Hmm. What about other data types that are defined before Data.Typeable.Internal is even defined? How do we get away with not having mkTrCon in scope? I think it's probably that they don't generate any Typeable evidence.

But mkTrCon itself requires no Typeable evidence. So one possibility would be to move it and the things it depends on into another module; or equivalently to move the bits of Internal that generate Typeable evidence somewhere else.

Another (inelegant) possibility would be to retain EvTypeable and continue to do that in the desugarer.

comment:9 Changed 11 months ago by simonpj

When zonking a CoreExpr, is there a need to zonk inside a Tickish?

Probably will never be used, but safer to do so.

Is it correct that the evVarsOfTerm are those free variables of the expression for which isEvVar is true

I believe so, yes

comment:10 Changed 11 months ago by nomeata

The error message, with a bit more detail, is

libraries/base/Data/Typeable/Internal.hs:618:5: error:
    • GHC internal error: ‘mkTrCon’ is not in scope during type checking, but it passed the renamer
      tcl_env of environment: [088 :-> Identifier[mkTrType::TypeRep
                                                              *, TopLevelLet],
                               089 :-> Identifier[mkTrCon::forall k (a :: k).
                                                           TyCon
                                                           -> [SomeTypeRep]
                                                           -> TypeRep a, TopLevelLet [] True],

Doesn’t that mean that mkTrCon actually is in scope, but somehow the lookup doesn't find it (different Unique maybe?)

comment:11 Changed 11 months ago by simonpj

Doesn’t that mean that mkTrCon actually is in scope

Looks odd. Use -dppr-debug to see the unique of the thing being looked up.

comment:12 Changed 11 months ago by nomeata

Ok, here is (part of) the deal:

  • tcLookupGlobal :: Name -> TcM TyThing looks things up in the global environment (getGblEnv). While compiling Data.Typeable.Internal, mkTrCon is not in the global environment.
  • If the lookup fails, it uses notFound, which, for some reason, prints the tcl_env of the *local* environment (lcl_env <- getLclEnv).
  • This shows us that mkTrCon is actually in the local environment! So presumably, we just have to use that.

I would have expected that tcLookup :: Name -> TcM TcTyThing (no Global in the name) would consult the local environment. It seems to consult the local type environment (local_env <- getLclTypeEnv). But when I tried that (in http://git.haskell.org/ghc.git/commitdiff/cb7deb6d0f36132594ccad3c86bddc7d7cdbb0dd) it somehow did not help. Will have to try harder, I guess.

comment:13 Changed 11 months ago by nomeata

Ok, I made progress. tcLookupId is the right thing to use here, I just need to use it in the right place :-)

Next problem:

libraries/base/GHC/Exception.hs:1:1: error:
    GHC internal error: ‘GHC.Exception.$tcArithException’ is not in scope during type checking, but it passed the renamer

I believe this is caused by the following

tyConRep :: TyCon -> TcS CoreExpr
-- Returns CoreExpr :: TyCon
tyConRep tc
  | Just tc_rep_nm <- tyConRepName_maybe tc
  = do { tc_rep_id <- tcLookupId tc_rep_nm
       ; return (Var tc_rep_id) }
  | otherwise
  = pprPanic "tyConRep" (ppr tc)

where the tcLookupId fails, because the type-checker does not know yet that GHC.Exception.$tcArithException exists (not sure if it exists at that time).

comment:14 Changed 11 months ago by simonpj

tcLookup... when I tried that it somehow did not help

tcLookupId is the right thing to use here

That's bizarre. tcLookupId calls tcLookup, so if the former succeeds, so should the latter (provided you deal with both ATcId and AGlobal results).

Last edited 11 months ago by simonpj (previous) (diff)

comment:15 Changed 11 months ago by nomeata

I was using lookupName previously, from the MonadThings instance, which goes through tcLookupGlobal; I believe that is the cause for the bizarriness:

instance MonadThings (IOEnv (Env TcGblEnv TcLclEnv)) where
    lookupThing = tcLookupGlobal

comment:16 Changed 11 months ago by simonpj

$tcArithException. Also bizarre. From what you say, it happens in an ordinary value definition, with no Typeable stuff in sight. I'm lost.

comment:17 Changed 11 months ago by simonpj

I was using lookupName previously

Yes, but then you said "..I would have expected that tcLookup :: Name -> TcM TcTyThing (no Global in the name) would consult the local environment. ... somehow did not help"

Anyway, you are past that roadblock now anyway, which is good.

comment:18 Changed 11 months ago by nomeata

Yes, but then you said "..I would have expected that tcLookup :: Name -> TcM TcTyThing (no Global in the name) would consult the local environment. ... somehow did not help"

yes, but I was not using it in all the places I should have – that bizzarness was simply a mistake by me, sorry for the confusion.

About $tcArithException :: TyCon – this value lives in GHC.Exception, but obviously it is not present in the Haskell source. Which phase is responsible for synthesizing these values? It seems that they are synthesized and added after TcInteract resolves the Typeable constraints (or, if they are created earlier, they are not added to the type checker’s local environment).

Last edited 11 months ago by simonpj (previous) (diff)

comment:19 Changed 11 months ago by nomeata

Ah, it seems I have two make sure mkTypeableBinds is called before simplifyTop in tcRnSrcDecls.

comment:20 Changed 11 months ago by simonpj

Ah, it seems I have two make sure mkTypeableBinds is called before simplifyTop in tcRnSrcDecls.

This is a stronger reason for deferring the desugaring of Typeable evidence: such evidence necessarily refers to top-level Haskell binding for the type representation of a type constructor defined in this module. e.g. To solve Typeable T we need to refer to T's type representation.

But we haven't generated those top-level bindings yet.

In general, such evidence-solving may take place before simplifyTop is called; e.g. in simplifyInfer.

Given this, better to defer to the desugarer I think, to postpone any evidence-solving that requires bindings that might be generated in this very module.

comment:21 Changed 11 months ago by nomeata

Given this, better to defer to the desugarer I think, to postpone any evidence-solving that requires bindings that might be generated in this very module.

So should I try this:

data EvTerm = EvExpr CoreExpr | EvTypeable EvTypeable

This is differs from the state before, because now the CoreExpr in an EvExpr can no longer refer to an EvTypeable… I cannot tell yet if that would happen or if it is a problem.

comment:22 Changed 11 months ago by simonpj

now the CoreExpr in an EvExpr can no longer refer to an EvTypeable

Well it can, via (Var d) where d is the Id of the typeable evidence. So I think it'll be fine

comment:23 Changed 11 months ago by nomeata

Hmpf, no matter how I shake it, it converges back to having many constructors for EvTerm.

At first I added only EvTypeable, because we have determined that we cannot create the Core for that during constraint solving.

But then I find code like this:

rewriteEvidence ev@(CtWanted { ctev_dest = dest
                             , ctev_loc = loc }) new_pred co
  = do { mb_new_ev <- newWanted loc new_pred
       ; MASSERT( tcCoercionRole co == ctEvRole ev )
       ; setWantedEvTerm dest
                   (mkEvCast (getEvTerm mb_new_ev)
                             (tcDowngradeRole Representational (ctEvRole ev) co))
       ; case mb_new_ev of
            Fresh  new_ev -> continueWith new_ev
            Cached _      -> stopWith ev "Cached wanted" }

where an arbitrary EvTerm, the result of getEvTerm needs to be casted. I cannot use Core’s Cast for that, because the EvTerm may be a EvTypeable. So seems that I need to add the EvCast constructor back to EvTerm … and bit by bit I am undoing the refactoring that I was hoping to do here…

Maybe the better thing to do is to leave all the existing constructors in place, and just add EvExpr :: CoreExpr -> EvTerm as an additional leaf constructor. This way, the existing code structure can remain.

comment:24 Changed 11 months ago by simonpj

I cannot use Core’s Cast for that, because the EvTerm may be a EvTypeable.

I think you can. getEvTerm calls ctEvTerm which always returns either an EvId (which we can do in Core) or an EvCoercion (ditto). Aside from coercions (alas) all evidence is represented just by an Id.

comment:25 Changed 11 months ago by nomeata

I think you can. getEvTerm calls ctEvTerm which always returns either an EvId (which we can do in Core) or an EvCoercion (ditto). Aside from coercions (alas) all evidence is represented just by an Id.

Ah, is that an invariant? Could we encode that in the types somehow?

comment:26 Changed 11 months ago by nomeata

I guess I can answer that myself, and will give it a try.

comment:27 Changed 11 months ago by Joachim Breitner <mail@…>

In 0e022e5/ghc:

Turn EvTerm (almost) into CoreExpr (#14691)

Ideally, I'd like to do

    type EvTerm = CoreExpr

and the type checker builds the evidence terms as it goes. This failed,
becuase the evidence for `Typeable` refers to local identifiers that are
added *after* the typechecker solves constraints. Therefore, `EvTerm`
stays a data type with two constructors: `EvExpr` for `CoreExpr`
evidence, and `EvTypeable` for the others.

Delted `Note [Memoising typeOf]`, its reference (and presumably
relevance) was removed in 8fa4bf9.

Differential Revision: https://phabricator.haskell.org/D4341

comment:28 Changed 7 months ago by adamgundry

Keywords: TypeCheckerPlugins added

@nomeata is this ticket now fully implemented?

comment:29 Changed 7 months ago by nomeata

Resolution: fixed
Status: newclosed

@nomeata is this ticket now fully implemented?

Yes, at least as good as I managed to do it (there is still the EvTypeable constructor, as explained in the commit message). But it is good enough for the libraries (e.g. [ghc-justdoit](http://hackage.haskell.org/package/ghc-justdoit)), so this can be considered done.

Note: See TracTickets for help on using tickets.