These two can be handled by adding a third case to the return type of findInstance and logging a warning instead of adding a constraint:
Lines 79 to 80 in fd926f0
NoOutputTypeName -> typeError $ InvalidInstanceHeadType instTy ImproperInstHead
OutputTypeVisiblePi -> typeError $ InvalidInstanceHeadType instTy ImproperInstTele
Lines 396 to 400 in fd926f0
case cands of
Left unblock -> do
reportSLn "tc.instance" 20 "Can't figure out target of instance goal. Postponing constraint."
addConstraint unblock $ FindInstance r m Nothing
Right cs -> findInstance m (Just cs)
It can't just be Left neverUnblock <$ warning ... because instance constraints can be retried even if their blocker hasn't changed.
This can be handled by turning the when into an if and returning HellNo ... instead of calling the continuation:
Lines 917 to 918 in fd926f0
when (d > maxDepth) $ typeError $ InstanceSearchDepthExhausted c a maxDepth
k
This can be handled by logging a warning and returning Nothing, letting the meta go unsolved:
Lines 564 to 565 in fd926f0
setCurrentRange (take' 1 $ map' snd sortedErrs) $
typeError $ InstanceNoCandidate t [ (candidateTerm c, err) | (c, err) <- sortedErrs ]
These two can be handled by adding a third case to the return type of `findInstance` and logging a warning instead of adding a constraint:
https://codeberg.org/1lab/mikan/src/commit/fd926f03995138c6925e12f60c34ebdd6d5a65cc/src/full/Mikan/TypeChecking/InstanceArguments.hs#L79-L80
https://codeberg.org/1lab/mikan/src/commit/fd926f03995138c6925e12f60c34ebdd6d5a65cc/src/full/Mikan/TypeChecking/InstanceArguments.hs#L396-L400
It can't just be `Left neverUnblock <$ warning ...` because instance constraints can be retried even if their blocker hasn't changed.
---
This can be handled by turning the `when` into an `if` and returning `HellNo ...` instead of calling the continuation:
https://codeberg.org/1lab/mikan/src/commit/fd926f03995138c6925e12f60c34ebdd6d5a65cc/src/full/Mikan/TypeChecking/InstanceArguments.hs#L917-L918
---
This can be handled by logging a warning and returning `Nothing`, letting the meta go unsolved:
https://codeberg.org/1lab/mikan/src/commit/fd926f03995138c6925e12f60c34ebdd6d5a65cc/src/full/Mikan/TypeChecking/InstanceArguments.hs#L564-L565