A Rewrite System for Type Checking Scoped Conformances

[dabrahams]

I'm posting this to capture results from this Slack thread, which will become inaccessible eventually.

The compiler can ensure soundness when there is no global coherence by applying a set of rewrite rules, and then using typechecking rules that would work when there is global coherence.

The crucial soundness problem solved is that a generic type can change dramatically (even in size or storage layout) based on conformances, due to the ability to store instances of associated types. As a result, a single spelling for a generic type in two different conformance contexts can represent a different type in each context. The additional type information injected by the rewrite rules allows the compiler distinguish these types. You can think of the rewrite process as a desugaring.

Crucial desirable properties of this scheme are:

1. Non-generic types such as Int can pass freely between conformance contexts.
2. Interfaces and API boundaries hold. For example, the caller of a generic function won't fail type-checking simply because of changes in that function's body; the user of a generic type won't fail type-checking due to changes to that type's private parts.
3. By construction, given a sound type-system for a language with global coherence, the soundness of a language without global coherence can be proven.
4. Nothing prevents the use in the same expression of differently-conforming instances of a generic type, except where it can affect soundness (where "can" includes possible changes behind API boundaries). For example, we can add the lengths of two differently-conforming arrays.

---

1. For each trait X we synthesize a second trait X' with same-shaped associated types.

   trait X { 
     type P: X
     // non-associated-type requirements…
   }
   
   trait X' { type P': X'}
   
   trait Y {
     type O: X
     // non-associated-type requirements…
   }
   
   trait Y' {
     type O': X'
   }
   
   trait Z {
     type M: Y
     type N: Y where M.O == N.O
     // non-associated-type requirements…
   }
   
   trait Z' {
     type M': Y'
     type N': Y' where M'.O' == N'.O'
   }

   and so on.

2. Every generic component is augmented with an additional type parameter for each of its type parameters, with a parallel set of constraints:

   fun f<A: X, B: X where A.P == B.P>() {}

   becomes

   fun f'<A: X, A': X', B: X, B': X' where A.P == B.P, A'.P' == B'.P'>() {}

   and so on.

   The extra parameters to generic types ensure that after the rewrite, pre-rewrite spellings are only the same type when they depend on the same set of conformances.

3. For every conformance declaration we generate a type declaration, which is passed to rewritten uses of generic components:

   conformance Int: X { type P = Int }
   type Int': X' { type P' = Int' }
   
   conformance Bool: X { type P = Int }
   type Bool': X' { type P' = Int' }
   
   // let j: Void = f<Int, Bool>()
   let j': Void = f<Int, Int', Bool, Bool'>()

Plain lexical scoping rules make scoped conformance work:

namespace Q {
  conformance Bool: X { type P = Bool }
  type Bool': X' { type P' = Bool' } 
  
  // let k: Void = f<Int, Bool>()
  let k': Void = f<Int, Int', Bool, Bool'>() // error
}

The error above is that f requires A.P == B.P, but in this context A.P is Int and B.P is Bool.