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
InferResult
s. 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
!