A4: Universe constraints — field sort levels must be ≤ inductive result level.
(
&mut self,
ctor_ty: &KExpr<M>,
n_params: usize,
ind_level: &KUniv<M>,
)
| 1916 | param_args: &[KExpr<M>], |
| 1917 | us: &[KUniv<M>], |
| 1918 | augmented_addrs: &[Address], |
| 1919 | ) -> Result<(), TcError<M>> { |
| 1920 | // Instantiate universe params |
| 1921 | let mut ty = self.instantiate_univ_params(ctor_ty, us)?; |
| 1922 | |
| 1923 | // Strip param foralls |
| 1924 | for _ in 0..n_params { |
| 1925 | let w = self.whnf(&ty)?; |
| 1926 | match w.data() { |
| 1927 | ExprData::All(_, _, _, body, _) => ty = body.clone(), |
| 1928 | _ => return Ok(()), // not enough foralls — ok |
| 1929 | } |
| 1930 | } |
| 1931 | |
| 1932 | // Simultaneously substitute param_args for the param binders. |
| 1933 | // After stripping n_params foralls, Var(0)..Var(n_params-1) in the body |
| 1934 | // refer to the params (Var(0) = innermost = last param). |
| 1935 | // simul_subst replaces Var(depth+i) with substs[i], so at depth=0: |
| 1936 | // Var(0) -> substs[0], Var(1) -> substs[1], ... |
| 1937 | // The params were bound outermost-first, so after stripping: |
| 1938 | // Var(n_params-1) = first param (outermost) |
| 1939 | // Var(0) = last param (innermost) |
| 1940 | // We need substs[i] = param_args[n_params-1-i] to reverse the order. |
| 1941 | let reversed_params: Vec<KExpr<M>> = |
| 1942 | param_args.iter().rev().cloned().collect(); |
| 1943 | ty = simul_subst(&mut self.env.intern, &ty, &reversed_params, 0); |
| 1944 | |
| 1945 | // Now check each remaining field domain |
| 1946 | self.check_nested_ctor_fields_loop(&ty, augmented_addrs) |
| 1947 | } |
| 1948 | |
| 1949 | /// Walk the remaining forall binders of a nested constructor type and check |
| 1950 | /// each field domain for positivity against the augmented address set. |
| 1951 | fn check_nested_ctor_fields_loop( |
| 1952 | &mut self, |
| 1953 | ty: &KExpr<M>, |
| 1954 | augmented_addrs: &[Address], |
| 1955 | ) -> Result<(), TcError<M>> { |
| 1956 | let w = self.whnf(ty)?; |
| 1957 | match w.data() { |
| 1958 | ExprData::All(_, _, dom, body, _) => { |
| 1959 | self.check_positivity_domain(dom, augmented_addrs)?; |
| 1960 | let saved = self.lctx.len(); |
| 1961 | let (open, _) = self.open_binder_anon(dom.clone(), body); |
| 1962 | let result = self.check_nested_ctor_fields_loop(&open, augmented_addrs); |
| 1963 | self.lctx.truncate(saved); |
| 1964 | result |
| 1965 | }, |
| 1966 | _ => Ok(()), // base case: return type — no more fields to check |
| 1967 | } |
| 1968 | } |
| 1969 |
no test coverage detected