Skip to content

Inferring multiple rhos for multiple equations causes a type conversion panic

Let's look at the ./test/cases/should-typecheck/rhoMultipleInferEvenSimpler-infer.hs test:

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

which causes the following panic:

    rhoMultipleEvenSimpler-infer: FAIL (0.01s)
      PprPanic "sigmaToRho_p" forall a54:mv-t53[1]:Type. a54
      CallStack (from HasCallStack):
        pprPanic, called at src/Type.hs:443:26 in typechecker-0.1.0.0-inplace:Type
        sigmaToRho_p, called at src/Tc/Gen/Pat.hs:209:13 in typechecker-0.1.0.0-inplace:Tc.Gen.Pat

The problem lies in the way we typecheck the LHS of match-expressions. Whenever we see a match-expression of arity n, we create n + 1 InferResults. This is because we need to make sure that all of the patterns that line up, and all of the expressions on the right hand side have matching types.

Here is the function that does exactly that:

tcMatches gamma mchs (Infer inferRes) = do
  -- The arity of match
  let arities = map tcArityVis mchs -- TODO: This doesn't handle EmptyCase
      arity   = head arities        -- TODO: Remove me
  unless (sameArity arities) $
    throwError (ArityMisMatch $
                pretty "Arity mismatch:" <+>
                pprListV mchs)
  -- Enough Expected types to push to the LHS of /all/ match-expressions.
  -- See Note [Expected type of patterns in tcMatchInfer]
  (irs, ir) <- updEnv pushAmbientTcLevel $ do
    irs <- replicateM arity newInferResult
    ir  <- newInferResult
    pure (irs, ir)
  mapM_ (\mch -> tcMatchInfer gamma mch irs ir) mchs
  -- Type of the LHS of all matches
  sigmas    <- mapM (fmap rhoToSigma . extractInferredResult) irs
  rho       <- extractInferredResult ir
  let final = appArrowR sigmas rho
  traceTc "tcMatches-Matches-Infer" (vsep [pretty "rho   =" <+> pretty rho
                                          ,pretty "final =" <+> pretty final])
  -- Final type of the match expressions
  fillInferResult final inferRes

Why is this problematic? because assume we have split our rhoMultipleInfereEvenSimpler function into the following categories:

LHSs: [['a', (x :: forall a. a)]
      ,[_, (x :: forall a. a)]
RHSs: [False
      ,True]

And we want to infer the type: rhoMultipleInferSimpler : Char -> (forall a1:Type. a1) -> Bool

This is how we want the patterns to line up with their types: LHS: ['a',_] : Char [(x :: forall a. a), (x :: forall a. a)] : forall a1:Type. a1

RHS: [False, True] : Bool

The way we achieve this is by doing fillInferResult over the inferred types, which will blow up when it encounters forall a1:Type. a1!

Edited by Artin Ghasivand