diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs index 4255e4aefe2e4fb0785e3b37c91c59b6ccb4d6c5..3a3231d2700b6675952ca0ba0ba4613380c1250b 100644 --- a/compiler/types/Coercion.hs +++ b/compiler/types/Coercion.hs @@ -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 diff --git a/compiler/types/Coercion.hs-boot b/compiler/types/Coercion.hs-boot index 75fdd77f5a932d2770d626e9a7cde6e9ae246222..15e45852df7a7eed410dfe687494fe539b047c86 100644 --- a/compiler/types/Coercion.hs-boot +++ b/compiler/types/Coercion.hs-boot @@ -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