Commit 86bba7d5 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Add missing check to isReflCoVar_maybe

isReflCoVar_maybe is called, by CoreLint, on all sorts of
Vars (tyvars, term vars, coercion vars).  But it was silently
assuming that it was always called on a CoVar, and as a result
could crash fatally.  This is the immediate cause of the panic
in Trac #15163.

It's easy to fix.

NB: this does not completely fix Trac #15163; more to come
parent 49a832dd
......@@ -360,12 +360,12 @@ splitForAllCo_maybe _ = Nothing
-------------------------------------------------------
-- and some coercion kind stuff
coVarTypes :: CoVar -> Pair Type
coVarTypes :: HasDebugCallStack => CoVar -> Pair Type
coVarTypes cv
| (_, _, ty1, ty2, _) <- coVarKindsTypesRole cv
= Pair ty1 ty2
coVarKindsTypesRole :: CoVar -> (Kind,Kind,Type,Type,Role)
coVarKindsTypesRole :: HasDebugCallStack => CoVar -> (Kind,Kind,Type,Type,Role)
coVarKindsTypesRole cv
| Just (tc, [k1,k2,ty1,ty2]) <- splitTyConApp_maybe (varType cv)
= let role
......@@ -420,10 +420,12 @@ mkRuntimeRepCo co
kind_co = mkKindCo co -- kind_co :: TYPE r1 ~ TYPE r2
-- (up to silliness with Constraint)
isReflCoVar_maybe :: CoVar -> Maybe Coercion
isReflCoVar_maybe :: Var -> Maybe Coercion
-- If cv :: t~t then isReflCoVar_maybe cv = Just (Refl t)
-- Works on all kinds of Vars, not just CoVars
isReflCoVar_maybe cv
| Pair ty1 ty2 <- coVarTypes cv
| isCoVar cv
, Pair ty1 ty2 <- coVarTypes cv
, ty1 `eqType` ty2
= Just (Refl (coVarRole cv) ty1)
| otherwise
......
......@@ -36,7 +36,7 @@ mkProofIrrelCo :: Role -> Coercion -> Coercion -> Coercion -> Coercion
isReflCo :: Coercion -> Bool
isReflexiveCo :: Coercion -> Bool
decomposePiCos :: Kind -> [Type] -> Coercion -> ([Coercion], Coercion)
coVarKindsTypesRole :: CoVar -> (Kind, Kind, Type, Type, Role)
coVarKindsTypesRole :: HasDebugCallStack => CoVar -> (Kind, Kind, Type, Type, Role)
coVarRole :: CoVar -> Role
mkCoercionType :: Role -> Type -> Type -> Type
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment