Commit 2b90356d authored by Richard Eisenberg's avatar Richard Eisenberg Committed by Marge Bot

Fix #14729 by making the normaliser homogeneous

This ports the fix to #12919 to the normaliser. (#12919 was about
the flattener.) Because the fix is involved, this is done by
moving the critical piece of code to Coercion, and then calling
this from both the flattener and the normaliser.

The key bit is: simplifying type families in a type is always
a *homogeneous* operation. See #12919 for a discussion of why
this is the Right Way to simplify type families.

Also fixes #15549.

test case: dependent/should_compile/T14729{,kind}
           typecheck/should_compile/T15549[ab]
parent aad05fb3
Pipeline #1973 failed with stages
in 394 minutes
......@@ -491,6 +491,10 @@ pmTopNormaliseType_maybe :: FamInstEnvs -> Bag EvVar -> Type
-- Behaves exactly like `topNormaliseType_maybe`, but instead of returning a
-- coercion, it returns useful information for issuing pattern matching
-- warnings. See Note [Type normalisation for EmptyCase] for details.
--
-- NB: Normalisation can potentially change kinds, if the head of the type
-- is a type family with a variable result kind. I (Richard E) can't think
-- of a way to cause trouble here, though.
pmTopNormaliseType_maybe env ty_cs typ
= do (_, mb_typ') <- liftD $ initTcDsForSolver $ tcNormalise ty_cs typ
-- Before proceeding, we chuck typ into the constraint solver, in case
......@@ -536,7 +540,7 @@ pmTopNormaliseType_maybe env ty_cs typ
tyFamStepper :: NormaliseStepper ([Type] -> [Type], [DataCon] -> [DataCon])
tyFamStepper rec_nts tc tys -- Try to step a type/data family
= let (_args_co, ntys) = normaliseTcArgs env Representational tc tys in
= let (_args_co, ntys, _res_co) = normaliseTcArgs env Representational tc tys in
-- NB: It's OK to use normaliseTcArgs here instead of
-- normalise_tc_args (which takes the LiftingContext described
-- in Note [Normalising types]) because the reduceTyFamApp below
......@@ -747,7 +751,7 @@ then
type we get if we rewrite type families but not data families or
newtypes.
(b) dcs is the list of data constructors "skipped", every time we normalise a
newtype to it's core representation, we keep track of the source data
newtype to its core representation, we keep track of the source data
constructor.
(c) core_ty is the rewritten type. That is,
pmTopNormaliseType_maybe env ty_cs ty = Just (src_ty, dcs, core_ty)
......
This diff is collapsed.
This diff is collapsed.
......@@ -2,7 +2,7 @@
--
-- FamInstEnv: Type checked family instance declarations
{-# LANGUAGE CPP, GADTs, ScopedTypeVariables, BangPatterns #-}
{-# LANGUAGE CPP, GADTs, ScopedTypeVariables, BangPatterns, TupleSections #-}
module FamInstEnv (
FamInst(..), FamFlavor(..), famInstAxiom, famInstTyCon, famInstRHS,
......@@ -60,7 +60,6 @@ import Var
import Pair
import SrcLoc
import FastString
import MonadUtils
import Control.Monad
import Data.List( mapAccumL )
import Data.Array( Array, assocs )
......@@ -1268,16 +1267,33 @@ topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Coercion, Type)
--
-- However, ty' can be something like (Maybe (F ty)), where
-- (F ty) is a redex.
--
-- Always operates homogeneously: the returned type has the same kind as the
-- original type, and the returned coercion is always homogeneous.
topNormaliseType_maybe env ty
= topNormaliseTypeX stepper mkTransCo ty
= do { ((co, mkind_co), nty) <- topNormaliseTypeX stepper combine ty
; return $ case mkind_co of
MRefl -> (co, nty)
MCo kind_co -> let nty_casted = nty `mkCastTy` mkSymCo kind_co
final_co = mkCoherenceRightCo Representational nty
(mkSymCo kind_co) co
in (final_co, nty_casted) }
where
stepper = unwrapNewTypeStepper `composeSteppers` tyFamStepper
stepper = unwrapNewTypeStepper' `composeSteppers` tyFamStepper
combine (c1, mc1) (c2, mc2) = (c1 `mkTransCo` c2, mc1 `mkTransMCo` mc2)
unwrapNewTypeStepper' :: NormaliseStepper (Coercion, MCoercionN)
unwrapNewTypeStepper' rec_nts tc tys
= mapStepResult (, MRefl) $ unwrapNewTypeStepper rec_nts tc tys
-- second coercion below is the kind coercion relating the original type's kind
-- to the normalised type's kind
tyFamStepper :: NormaliseStepper (Coercion, MCoercionN)
tyFamStepper rec_nts tc tys -- Try to step a type/data family
= let (args_co, ntys) = normaliseTcArgs env Representational tc tys in
= let (args_co, ntys, res_co) = normaliseTcArgs env Representational tc tys in
case reduceTyFamApp_maybe env Representational tc ntys of
Just (co, rhs) -> NS_Step rec_nts rhs (args_co `mkTransCo` co)
Just (co, rhs) -> NS_Step rec_nts rhs (args_co `mkTransCo` co, MCo res_co)
_ -> NS_Done
---------------
......@@ -1301,21 +1317,36 @@ normalise_tc_app tc tys
= -- A type-family application
do { env <- getEnv
; role <- getRole
; (args_co, ntys) <- normalise_tc_args tc tys
; (args_co, ntys, res_co) <- normalise_tc_args tc tys
; case reduceTyFamApp_maybe env role tc ntys of
Just (first_co, ty')
-> do { (rest_co,nty) <- normalise_type ty'
; return ( args_co `mkTransCo` first_co `mkTransCo` rest_co
, nty ) }
; return (assemble_result role nty
(args_co `mkTransCo` first_co `mkTransCo` rest_co)
res_co) }
_ -> -- No unique matching family instance exists;
-- we do not do anything
return (args_co, mkTyConApp tc ntys) }
return (assemble_result role (mkTyConApp tc ntys) args_co res_co) }
| otherwise
= -- A synonym with no type families in the RHS; or data type etc
-- Just normalise the arguments and rebuild
do { (args_co, ntys) <- normalise_tc_args tc tys
; return (args_co, mkTyConApp tc ntys) }
do { (args_co, ntys, res_co) <- normalise_tc_args tc tys
; role <- getRole
; return (assemble_result role (mkTyConApp tc ntys) args_co res_co) }
where
assemble_result :: Role -- r, ambient role in NormM monad
-> Type -- nty, result type, possibly of changed kind
-> Coercion -- orig_ty ~r nty, possibly heterogeneous
-> CoercionN -- typeKind(orig_ty) ~N typeKind(nty)
-> (Coercion, Type) -- (co :: orig_ty ~r nty_casted, nty_casted)
-- where nty_casted has same kind as orig_ty
assemble_result r nty orig_to_nty kind_co
= ( final_co, nty_old_kind )
where
nty_old_kind = nty `mkCastTy` mkSymCo kind_co
final_co = mkCoherenceRightCo r nty (mkSymCo kind_co) orig_to_nty
---------------
-- | Normalise arguments to a tycon
......@@ -1323,21 +1354,23 @@ normaliseTcArgs :: FamInstEnvs -- ^ env't with family instances
-> Role -- ^ desired role of output coercion
-> TyCon -- ^ tc
-> [Type] -- ^ tys
-> (Coercion, [Type]) -- ^ co :: tc tys ~ tc new_tys
-> (Coercion, [Type], CoercionN)
-- ^ co :: tc tys ~ tc new_tys
-- NB: co might not be homogeneous
-- last coercion :: kind(tc tys) ~ kind(tc new_tys)
normaliseTcArgs env role tc tys
= initNormM env role (tyCoVarsOfTypes tys) $
normalise_tc_args tc tys
normalise_tc_args :: TyCon -> [Type] -- tc tys
-> NormM (Coercion, [Type]) -- (co, new_tys), where
-- co :: tc tys ~ tc new_tys
-> NormM (Coercion, [Type], CoercionN)
-- (co, new_tys), where
-- co :: tc tys ~ tc new_tys; might not be homogeneous
-- res_co :: typeKind(tc tys) ~N typeKind(tc new_tys)
normalise_tc_args tc tys
= do { role <- getRole
; (cois, ntys) <- zipWithAndUnzipM normalise_type_role
tys (tyConRolesX role tc)
; return (mkTyConAppCo role tc cois, ntys) }
where
normalise_type_role ty r = withRole r $ normalise_type ty
; (args_cos, nargs, res_co) <- normalise_args (tyConKind tc) (tyConRolesX role tc) tys
; return (mkTyConAppCo role tc args_cos, nargs, res_co) }
---------------
normaliseType :: FamInstEnvs
......@@ -1363,10 +1396,9 @@ normalise_type ty
go (TyConApp tc tys) = normalise_tc_app tc tys
go ty@(LitTy {}) = do { r <- getRole
; return (mkReflCo r ty, ty) }
go (AppTy ty1 ty2)
= do { (co, nty1) <- go ty1
; (arg, nty2) <- withRole Nominal $ go ty2
; return (mkAppCo co arg, mkAppTy nty1 nty2) }
go (AppTy ty1 ty2) = go_app_tys ty1 [ty2]
go (FunTy ty1 ty2)
= do { (co1, nty1) <- go ty1
; (co2, nty2) <- go ty2
......@@ -1393,6 +1425,57 @@ normalise_type ty
co right_co
, mkCoercionTy right_co ) }
go_app_tys :: Type -- function
-> [Type] -- args
-> NormM (Coercion, Type)
-- cf. TcFlatten.flatten_app_ty_args
go_app_tys (AppTy ty1 ty2) tys = go_app_tys ty1 (ty2 : tys)
go_app_tys fun_ty arg_tys
= do { (fun_co, nfun) <- go fun_ty
; case tcSplitTyConApp_maybe nfun of
Just (tc, xis) ->
do { (second_co, nty) <- go (mkTyConApp tc (xis ++ arg_tys))
-- flatten_app_ty_args avoids redundantly processing the xis,
-- but that's a much more performance-sensitive function.
-- This type normalisation is not called in a loop.
; return (mkAppCos fun_co (map mkNomReflCo arg_tys) `mkTransCo` second_co, nty) }
Nothing ->
do { (args_cos, nargs, res_co) <- normalise_args (typeKind nfun)
(repeat Nominal)
arg_tys
; role <- getRole
; let nty = mkAppTys nfun nargs
nco = mkAppCos fun_co args_cos
nty_casted = nty `mkCastTy` mkSymCo res_co
final_co = mkCoherenceRightCo role nty (mkSymCo res_co) nco
; return (final_co, nty_casted) } }
normalise_args :: Kind -- of the function
-> [Role] -- roles at which to normalise args
-> [Type] -- args
-> NormM ([Coercion], [Type], Coercion)
-- returns (cos, xis, res_co), where each xi is the normalised
-- version of the corresponding type, each co is orig_arg ~ xi,
-- and the res_co :: kind(f orig_args) ~ kind(f xis)
-- NB: The xis might *not* have the same kinds as the input types,
-- but the resulting application *will* be well-kinded
-- cf. TcFlatten.flatten_args_slow
normalise_args fun_ki roles args
= do { normed_args <- zipWithM normalise1 roles args
; let (xis, cos, res_co) = simplifyArgsWorker ki_binders inner_ki fvs roles normed_args
; return (map mkSymCo cos, xis, mkSymCo res_co) }
where
(ki_binders, inner_ki) = splitPiTys fun_ki
fvs = tyCoVarsOfTypes args
-- flattener conventions are different from ours
impedance_match :: NormM (Coercion, Type) -> NormM (Type, Coercion)
impedance_match action = do { (co, ty) <- action
; return (ty, mkSymCo co) }
normalise1 role ty
= impedance_match $ withRole role $ normalise_type ty
normalise_tyvar :: TyVar -> NormM (Coercion, Type)
normalise_tyvar tv
= ASSERT( isTyVar tv )
......
......@@ -99,7 +99,7 @@ module Type (
mkTyCoVarBinder, mkTyCoVarBinders,
mkTyVarBinders,
mkAnonBinder,
isAnonTyCoBinder, isNamedTyCoBinder,
isAnonTyCoBinder,
binderVar, binderVars, binderType, binderArgFlag,
tyCoBinderType, tyCoBinderVar_maybe,
tyBinderType,
......@@ -1681,10 +1681,6 @@ isAnonTyCoBinder :: TyCoBinder -> Bool
isAnonTyCoBinder (Named {}) = False
isAnonTyCoBinder (Anon {}) = True
isNamedTyCoBinder :: TyCoBinder -> Bool
isNamedTyCoBinder (Named {}) = True
isNamedTyCoBinder (Anon {}) = False
tyCoBinderVar_maybe :: TyCoBinder -> Maybe TyCoVar
tyCoBinderVar_maybe (Named tv) = Just $ binderVar tv
tyCoBinderVar_maybe _ = Nothing
......
{-# LANGUAGE ExplicitForAll, PolyKinds, TypeFamilies, DataKinds #-}
module T14729 where
import Data.Kind
data P k :: k -> Type
type family F a
type instance F Int = Bool
x :: forall (x :: Bool). P (F Int) x
x = undefined
y = x
TYPE SIGNATURES
x :: forall (x :: Bool). P (F Int) (x |> Sym (T14729.D:R:FInt[0]))
y :: forall (x :: Bool). P Bool x
TYPE CONSTRUCTORS
type family F{1} :: * -> *
roles nominal
data type P{2} :: forall k -> k -> *
roles nominal phantom
COERCION AXIOMS
axiom T14729.D:R:FInt :: F Int = Bool
FAMILY INSTANCES
type instance F Int = Bool -- Defined at T14729.hs:10:15
Dependent modules: []
Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
integer-gmp-1.0.2.0]
:seti -XPolyKinds -XDataKinds -XExplicitForAll -XTypeFamilies
import Data.Kind
data P k :: k -> Type
type family F a
type instance F Int = Bool
:kind! forall (x :: Bool). P (F Int) x
forall (x :: Bool). P (F Int) x :: *
= P Bool x
......@@ -64,3 +64,5 @@ test('T15076', normal, compile, [''])
test('T15076b', normal, compile, [''])
test('T15076c', normal, compile, [''])
test('T15829', normal, compile, [''])
test('T14729', normal, compile, ['-ddump-types -fprint-typechecker-elaboration -fprint-explicit-coercions'])
test('T14729kind', normal, ghci_script, ['T14729kind.script'])
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
module T15549a where
import Data.Proxy
import Data.Void
data family Sing (a :: k)
data instance Sing (z :: Void)
type family Rep a
class SGeneric a where
sTo :: forall (r :: Rep a). Sing r -> Proxy a
type instance Rep Void = Void
instance SGeneric Void where
sTo x = case x of
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
module T15549b where
import Data.Kind (Type)
newtype Identity a = Identity a
newtype Par1 a = Par1 a
data family Sing :: forall k. k -> Type
data instance Sing :: forall k. k -> Type
type family Rep1 (f :: Type -> Type) :: Type -> Type
type instance Rep1 Identity = Par1
type family From1 (z :: f a) :: Rep1 f a
type instance From1 ('Identity x) = 'Par1 x
und :: a
und = und
f :: forall (a :: Type) (x :: Identity a). Sing x
f = g
where g :: forall (a :: Type) (f :: Type -> Type) (x :: f a). Sing x
g = seq (und :: Sing (From1 x)) und
......@@ -663,3 +663,5 @@ test('T14761c', normal, compile, [''])
test('T16008', normal, compile, [''])
test('T16033', normal, compile, [''])
test('T16141', normal, compile, ['-O'])
test('T15549a', normal, compile, [''])
test('T15549b', normal, compile, [''])
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