Better local inference for identity types

[fizruk]

A side question for @fizruk : For some reason, rzk does not seem able to infer the type of (τ, refl) in the expression Σ (τ : extension-type σ), (( τ, refl) =_{homotopy-extension-type σ} th) (src/simplicial-hott/04-extension-types.rzk.md, line 55), if I do not explicitly specify which equality type I am talking about (i.e. if I omit the _{homotopy-extension-type σ}. Does this make sense to you, or something it should be able to do?

Here's the definition in question:

https://github.com/rzk-lang/sHoTT/blob/1b1ff2d71ae374be1d05f74cff0db45906d49c59/src/simplicial-hott/04-extension-types.rzk.md?plain=1#L52-L61

The problem is that the typechecker currently only considers inferring type from the left argument of the identity type, but here we need infer it from the right one. It should be possible to have a simple fix here, will try to fit in the next release :)

Originally posted by @fizruk in rzk-lang/sHoTT#88 (comment)

Relevant code in the TypeChecker:

rzk/rzk/src/Rzk/TypeCheck.hs

Lines 2614 to 2618 in aeaac04

	TypeId x Nothing y -> do
	x' <- inferAs universeT x
	tA <- typeOf x'
	y' <- typecheck y tA
	return (typeIdT x' (Just tA) y')