hcompU eta rule in conversion checker loses solution

[SquidDev]

Agda.TypeChecking.Conversion has a rule to eta-expand applications of hcomp.

agda/src/full/Agda/TypeChecking/Conversion.hs

Lines 442 to 451 in 4ffbfd7

	Def q es | Just q == mHComp, Just (sl:s:args@[phi,u,u0]) <- allApplyElims es
	, Sort (Type lvl) <- unArg s
	, Just unglueU <- mUnglueU, Just subIn <- mSubIn
	-> do
	let l = Level lvl
	ty <- el' (pure $ l) (pure $ unArg u0)
	let bA = subIn `apply` [sl,s,phi,u0]
	let mkUnglue m = apply unglueU $ [argH l] ++ map (setHiding Hidden) [phi,u] ++ [argH bA,argN m]
	reportSDoc "conv.hcompU" 20 $ prettyTCM (ty,mkUnglue m,mkUnglue n)
	compareTerm cmp ty (mkUnglue m) (mkUnglue n)

However, currently this does not trigger as we look up SUBIN as a primitive rather than a builtin, so it's always treated as undefined:

agda/src/full/Agda/TypeChecking/Conversion.hs

Line 403 in 4ffbfd7

mSubIn <- getPrimitiveTerm' builtinSubIn

However, this rule may be too over-eager and when active can cause failures, as such as seen in this test run (in the defition of lCancelP). @plt-amy informs we we probably need some guards here to avoid over-eagerly applying this rule.

[SquidDev]

Thank you! You're the best!