The pattern judgement needs a new InferResult that can hold sigma-types.

Unlike expressions, patterns can actually get sigma types during inference. This is clearly stated in the signature of the |-pat judgement, and can be easily observed in the Pat-SigInfer rule. This has two implications:

• We can't use the normal InferResult datatype for patterns, because it can only hold a rho-type. Let's call the new datatype PatInferResult.
• We still need to do some kind of fillInferResult on PatInferResult, which in some cases, could emit equalities between sigma-types.

Here are some of the tests that reflect the need for PatInferResult:

rhoMultipleInfer True  = \(x :: forall a. a -> a -> a) -> \y           -> \(z :: Int) -> True
rhoMultipleInfer False = \(x :: forall a. a -> a -> a) -> \(y :: Bool) -> \z          -> True

rhoMultipleInferEvenSimpler 'a' (x :: forall a. a) = False
rhoMultipleInferEvenSimpler _   (x :: forall a. a) = True

higherRankLambda = \(x :: forall a. a -> a -> a) -> \y -> \(z :: Int) -> True

rhoMultipleInferSimple 'a' = \(x :: forall a. a) (y :: Integer) -> False
rhoMultipleInferSimple _   = \(x :: forall a. a) (y :: Integer) -> True

All of these fail with the following stack trace:

CallStack (from HasCallStack):
        pprPanic, called at src/HTC/Type.hs:467:26 in HTC-0.1.0.0-inplace:HTC.Type
        sigmaToRho_p, called at src/HTC/Tc/Gen/Pat.hs:287:13 in HTC-0.1.0.0-inplace:HTC.Tc.Gen.Pat

Here is the code that is causing the panic:

-- | Rule: Pat-SigInfer
tcPat gamma sigs (TAnnT p ty) (Infer inferResult) = do
  let amb_lvl = gammaTcLevel gamma
  tvbs <- tcBindTyVars gamma (fv ty)
  let extended = modifyScopedTyVarsGamma (tvbs <>) gamma
  sigma <- tcTyp extended ty (Check typeSigma)
  let rho = sigmaToRho_p sigma
  delta <- tcPat extended sigs p (Check sigma)
  fillInferResult amb_lvl rho inferResult
  traceRuleTc "tcPat" "Pat-SigInfer" $
    vsep [pretty "tvbs  =" <+> pretty tvbs
         ,pretty "rho   =" <+> pretty rho
         ,pretty "delta =" <+> pretty delta]
  let delta' = modifyScopedTyVarsDelta (tvbs <>) delta
  checkDeltaInvariants delta'
  pure delta'

This actually counts as a deviation too! because there are no rhos in the Pat-SigInfer rule!