     }
   }
 
-  private func visitDataType(
+  // swiftlint:disable function_parameter_count
+  private func completeDataType(
     _ name: QualifiedName,
-    _ origType: Type<TT>, _ substType: Type<TT>,
-    _ constructors: [Opened<QualifiedName, TT>]
-  ) -> Lowering {
-    if let asNat = dataTypeAsTrivialNat(name, origType, constructors) {
-      return asNat
-    }
+    _ origType: Type<TT>, _ substType: Type<TT>, _ elims: [Elim<TT>],
+    _ constructors: [Opened<QualifiedName, TT>],
+    _ lowering: Lowering
+  ) {
+    if completeDataTypeAsTrivialNat(name, substType, constructors, lowering) {
+      return
+    }
+
+    var indices = Context()
+    var curTy = origType
+    while case let .pi(indexTy, next) = curTy {
+      indices.append((wildcardName, indexTy))
+      curTy = next
+    }
+    let environment = Environment(indices)
 
     var hasOnlyTrivialCons = true
-    var forceAddressOnly = false
     var loweredConstructors = [DataType.Constructor]()
     loweredConstructors.reserveCapacity(constructors.count)
     for constructor in constructors {

  }

  private func withCachedKey(
    _ key: QualifiedName, _ f: (QualifiedName) -> Lowering) -> Lowering {
    guard !self.inProgressLowerings.contains(key) else {
      return RecursiveLowering(key)
    }

    self.inProgressLowerings.insert(key)
    let result = f(key)
    self.inProgressLowerings.remove(key)
    return result
  }
}

private class RecursiveLowering: TypeConverter.Lowering {
  init(_ name: QualifiedName) {
    super.init(type: BoxType(name),
               isTrivial: false, isAddressOnly: false)
  }
}

private class TrivialLowering: TypeConverter.Lowering {
  init(_ type: GIRType) {
    super.init(type: type, isTrivial: true, isAddressOnly: false)
  }
}

private class NonTrivialLowering: TypeConverter.Lowering {
  init(_ type: GIRType) {
    super.init(type: type, isTrivial: false, isAddressOnly: false)
  }
}

private class TrivialAddressOnlyLowering: TypeConverter.Lowering {
  init(_ type: GIRType) {
    super.init(type: type, isTrivial: true, isAddressOnly: true)
  }
}

private class AddressOnlyLowering: TypeConverter.Lowering {
  init(_ type: GIRType) {
    super.init(type: type, isTrivial: false, isAddressOnly: true)
  }
}

        guard let bind = tc.signature.lookupMetaBinding(mv) else {
          fatalError("Unbound meta!?")
        }
        return self.lower(bind.body, in: env)
      case .variable(_):
        fatalError()
      }
    case .equal(_, _, _):
      fatalError("FIXME: Emit metadata here")
