[GHC] #15952: Reduce zonking-related invariants in the type checker

[GHC]

#15952: Reduce zonking-related invariants in the type checker
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  task              |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.6.2
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 I have not reviewed the code, but just responding to comment:7.

 I agree about adding `ArgFlag` to `FunTy`, but not the way you probably
 want.

 I see `FunTy` as an abbreviation of `ForAllTy`, where the argument is
 relevant (preserved at runtime) and non-dependent (cannot appear in the
 rest of the type). Morally (in my opinion), we should have `ForAllTy`
 store a `TyCoBinder`, which stores either a `Named TyCoVarBinder` or an
 `Anon Type`. The `TyCoVarBinder` is a pair containing a `TyVar` and an
 `ArgFlag`. This `ForAllTy` should be called `PiTy`. It was implemented en
 route to the TypeInType patch but then `FunTy` was re-extracted from it
 for performance reasons.

 "Adding `ArgFlag` to `FunTy`" really means that the primordial `PiTy` now
 stores either a `Named (ArgFlag, TyVar)` or an `Anon (ArgFlag, Type)`.
 (I've rewritted `TyCoVarBinder` as `(ArgFlag, TyVar)` to simplify the
 presentation... and to ignore coercion variables, which can indeed safely
 be ignore in these parts.) But looking at this definition, we see an
 "obvious" refactor: store a `(NamedFlag, ArgFlag, TyVar)` where
 `NamedFlag` is a `Bool` cognate that says whether or not the quantifier is
 dependent. In the end, though, this information is needed only for
 performance reasons, as we can always treat quantifiers as dependent, but
 some usage sites won't take advantage of this capability. So that leaves
 us with `(ArgFlag, TyVar)` as the payload of the binder part of a `PiTy`
 (along with the "body" part, containing a `Type`). In other words:

 {{{#!hs
 data Type = ... | PiTy (ArgFlag, TyVar) Type | ...
 }}}

 Now, consider this code that we might try to compile:

 {{{#!hs
 data Dict :: Constraint -> Type where
   MkDict :: c => Dict c
 foo :: forall (x :: Proxy (MkDict :: Dict c)). Proxy x -> ()
 }}}

 What's the representation of the type of `foo`? It should be something
 like

 {{{#!hs
 foo :: PiTy (Specified, c :: Constraint) $
        PiTy (Inferred, ct :: c) $
        PiTy (Specified, x :: Proxy (Dict c) (MkDict c ct)) $
        PiTy (Required, _ :: Proxy (Proxy (Dict c) (MkDict c ct)) x) $
        unitTy
 }}}

 Now we have a usage site of `foo`. We instantiate this type. But,
 critically, '''how do we instantiate `ct`'''? Do we (a) emit an wanted
 constraint `c`, or (b) create a fresh unification variable `alpha` and
 then unify it with the right part of the type of the passed argument to
 `foo`? This choice matters -- it's conceivable that the solver in strategy
 (a) will find a different solution for `ct` than unification would come up
 with (in a situation with incoherency -- which normally does not imperil
 the type system).

 The bottom line here is that we need to indicate, for implicit arguments,
 precisely how GHC should try to infer them when they are omitted. Note
 that Agda does this: unification is indicated by single braces and solving
 is indicated by double braces. Currently, `ArgFlag` says when an argument
 is implicit. In the future, though, I think it will additionally need to
 specify an instantiation strategy for implicit arguments. To wit, we might
 have

 {{{#!hs
 data InstStrategy = Solve | Unify
 data ArgFlag = Inferred InstStrategy | Specified InstStrategy | Required
 }}}

 or possibly

 {{{#!hs
 data InstStrategy = Solve | Unify
 data VisibleInstAllowed = CanBeVisible | CannotBeVisible
 data ArgFlag = Invisible InstStrategy VisibleInstAllowed | Visible
 }}}

 Zooming back to the present: should we add `ArgFlag` to `FunTy`? I say:
 "no", because the current `ArgFlag` doesn't scale to the situation
 described above. Instead -- if we don't want to buy into the more
 elaborate scheme above -- we should make a new

 {{{#!hs
 data NonDepArgFlag   -- rename me
   = SolvedFor
   | Visible  -- I wish I could just reuse Required but no TDNR
 }}}

 and then add that to `FunTy`. This approach then naturally scales up to
 the more elaborate scheme described above. It also has the added bonus of
 not using the three-way `ArgFlag` to describe a situation which currently
 only has 2 possibilities.

 -------------------------------------

 Frustrating about #15918. But I agree with your analysis here. As long as
 we have two different equality relations (the one where `Type ~
 Constraint` and the one where it doesn't), this problem will persist. And
 I think trying to cheat by avoiding writing all these extra functions will
 fail. As to the idea of simplifying `mkCastTy` in favor of complicating
 `tcSplitXXX`, I think that might work fine... but I don't think it will
 save sweat or tears. We would need to have `tc` variants of all the
 splitting functions instead of all the making functions. And the problems
 we'll run into will be the same. I favor doing the work at construction,
 because I conjecture that we construct less often than we split, and it
 will make inspecting dumps easier (because we'll know that things that
 look different really are different).

 And I don't think that having, e.g., `mkTcCastTy` is as bad as the
 nakedness business. The naked casts were a nasty, fragile hack, using
 `Refl` in a way it was never intended. `mkTcCastTy`, on the other hand, is
 a perfectly sensible operation to build a type in a way so that types we
 consider equal have identical representations. The downside to the new
 approach is that it requires more code duplication, etc., than the naked-
 casts trick.

 --------------------------

 About #15799: That bug requires #12045 to witness, though the underlying
 fault exists in HEAD. I never drilled down to figure out how #12045
 triggers it.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15952#comment:8>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler