jonoodle @ionchy@types.pl

I just need elasticsearch to stay alive for like a minute

did I post the original thread on here as well lol
the paper might honestly predate this place being a real contender for announcing actual things lol

never mind I've just realized that my other problem isn't a problem at all and that type checking is failing because it's supposed to fail. good thing the principled manners of the type system is there to catch me when I'm thinking silly things even though I think it's the type system that's wrong all the time lol

I wish I could know what levels variables were used at going on
I would rather not have to unify-and-solve for them

puzzles for tomorrow. for now I've got to go home bc I have computer architecture early tmrw morning and learning more Verilog :/

but I can also grow the level by cumul
then it doesn't matter what level the variable is
blasphemous

hm. this is a different bug but I think I could justify shrinking the level of any variable from the context. that's very strange

I'm not sure how to proceed. I can't just make up a larger level to check against a. I suppose I could synth the type of a and compare against the type of b, but then I'd need to reconcile the mismatching levels, and it seems rather incorrect to take a max of levels here rather than isolated in a cumulativity judgement. I don't think I want to make b a a check judgement, I don't think, since dependent applications aren't? but if b a were checked against B at a particular level I could infer the type of a, making sure that its level isn't too big, and then reconstruct A → B to check against b at the given level

I've never seen the James Yoo singing lore...

this is the rule

Γ ⊢ b ⇑ A → B @ j
Γ ⊢ a ⇓ A @ j
---------------
Γ ⊢ b a ⇑ B @ j

except this breaks when b gets inferred at a smaller level such that a fails to check at that level lol

lmao my inference algorithm is having trouble with domains at smaller levels

my original twitter thread was good imo
I don't think anything has changed since then

no questions at this time thanks

what am I supposed to say abt the paper other than "it's out" I barely remember the contents

brain hurts

lmao I got it to type check but I don't know why and I have a bunch of inferred arguments I can't mentally deduce

(Set
 (lsuc (lsuc (lsuc (lsuc (lsuc ℓ)))) ⊔
  lsuc (lsuc (lsuc (lsuc (lsuc ℓ₁))))
  ⊔ lsuc (lsuc (lsuc (lsuc (lsuc ℓ₂))))
  ⊔ lsuc (lsuc _ℓ₂_72)
  ⊔ lsuc (lsuc _ℓ_75)
  ⊔ lsuc (lsuc _ℓ₁_76)))
is not less or equal than
(Set (lsuc (lsuc ℓ) ⊔ lsuc (lsuc ℓ₁) ⊔ lsuc (lsuc ℓ₂)))

hell world

Agda please I beg stop solving down to lzero I just need a placeholder whilst I think