Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC

Commits:

15 changed files:

Changes:

  • changelog.d/T27994
    1 
    +section: compiler
    2 
    +issues: #27994
    3 
    +mrs: !16842
    4 
    +synopsis:
    5 
    +  Fix a compiler Lint error in a heavily kind-polymorphic program
    6 
    +description:
    7 
    +  There was a subtle bug deep in the code for computing functional dependencies for type families.

  • compiler/GHC/Core/Coercion/Axiom.hs
    ... ... @@ -277,8 +277,8 @@ data CoAxBranch
    277 277 
            -- See Note [CoAxBranch type variables]
    278 278 
         , cab_eta_tvs  :: [TyVar]
    279 279 
            -- ^ Eta-reduced tyvars
    280 
    -       -- cab_tvs and cab_lhs may be eta-reduced; see
    281 
    -       -- Note [Eta reduction for data families]
    280 
    +       -- For a data family (only) cab_tvs and cab_lhs may be eta-reduced
    281 
    +       -- See Note [Eta reduction for data families]
    282 282 
         , cab_cvs      :: [CoVar]
    283 283 
           -- ^ Bound coercion variables
    284 284 
            -- Always empty, for now.
    ... ... @@ -286,8 +286,14 @@ data CoAxBranch
    286 286 
            -- in GHC.Tc.TyCl
    287 287 
         , cab_roles    :: [Role]
    288 288 
            -- ^ See Note [CoAxBranch roles]
    289 
    +
    289 290 
         , cab_lhs      :: [Type]
    290 291 
            -- ^ Type patterns to match against
    292 
    +       -- For a data family `cab_lhs` may be shorter than the arity
    293 
    +       --     of the data type
    294 
    +       -- For a type family `cab_lhs` is exactly the family arity
    295 
    +       -- See Note [Eta reduction for data families]
    296 
    +
    291 297 
         , cab_rhs      :: Type
    292 298 
            -- ^ Right-hand side of the equality
    293 299 
            -- See Note [CoAxioms are homogeneous]

  • compiler/GHC/Core/Predicate.hs
    ... ... @@ -36,7 +36,7 @@ module GHC.Core.Predicate (
    36 36
    37 37 
       -- Equality left-hand sides
    38 38 
       CanEqLHS(..), canEqLHS_maybe, canTyFamEqLHS_maybe,
    39 
    -  canEqLHSKind, canEqLHSType, eqCanEqLHS
    39 
    +  canEqLHSKind, canEqLHSType, eqCanEqLHS, saturatedFamApp_maybe
    40 40
    41 41 
       ) where
    42 42
    ... ... @@ -61,6 +61,8 @@ import GHC.Utils.Misc
    61 61 
     import GHC.Utils.Panic
    62 62 
     import GHC.Data.FastString
    63 63
    64 
    +import GHC.Exts( inline )
    65 
    +
    64 66
    65 67 
     {- *********************************************************************
    66 68 
     *                                                                      *
    ... ... @@ -700,7 +702,9 @@ types/kinds are fully settled and zonked.
    700 702 
     -- See also Note [Ordering of implicit variables] in "GHC.Rename.HsType"
    701 703
    702 704 
     scopedSort :: [Var] -> [Var]
    703 
    -scopedSort = go [] []
    705 
    +scopedSort xs
    706 
    +  | null xs   = []
    707 
    +  | otherwise = go [] [] xs
    704 708 
       where
    705 709 
         go :: [Var] -- already sorted, in reverse order
    706 710 
            -> [TyCoVarSet] -- each set contains all the variables which must be placed
    ... ... @@ -781,13 +785,19 @@ canEqLHS_maybe xi
    781 785 
       | otherwise
    782 786 
       = canTyFamEqLHS_maybe xi
    783 787
    784 
    -canTyFamEqLHS_maybe :: Type -> Maybe CanEqLHS
    785 
    -canTyFamEqLHS_maybe xi
    788 
    +saturatedFamApp_maybe :: Type -> Maybe (TyCon,[Type])
    789 
    +saturatedFamApp_maybe xi
    786 790 
       | Just (tc, args) <- tcSplitTyConApp_maybe xi
    787 791 
       , isTypeFamilyTyCon tc
    788 792 
       , args `lengthIs` tyConArity tc
    789 
    -  = Just $ TyFamLHS tc args
    793 
    +  = Just (tc,args)
    794 
    +  | otherwise
    795 
    +  = Nothing
    790 796
    797 
    +canTyFamEqLHS_maybe :: Type -> Maybe CanEqLHS
    798 
    +canTyFamEqLHS_maybe xi
    799 
    +  | Just (tc, args) <- inline saturatedFamApp_maybe xi
    800 
    +  = Just $ TyFamLHS tc args
    791 801 
       | otherwise
    792 802 
       = Nothing
    793 803

  • compiler/GHC/Core/TyCo/FVs.hs
    ... ... @@ -1159,10 +1159,12 @@ nice tight loops.
    1159 1159 
     {-# INLINE afvFolder #-}   -- See Note [Any-free-var folder]
    1160 1160 
     afvFolder :: TyCoFolder (FV (BoundVars, TyCoVar -> Bool) DM.Any)
    1161 1161 
     -- 'afvFolder' is short for "any-free-var folder", good for checking
    1162 
    ---   if any /deep/ free var of a type satisfies a predicate `check_fv`
    1162 
    +--   if any /shallow/ free var of a type satisfies a predicate `check_fv`
    1163 1163 
     -- The "env" of the (FV env Any) is a pair (bvs,pred) of
    1164 1164 
     --    the bound variables (which are definitely not free), and
    1165 1165 
     --    an "interesting var" predicate which the client supplies
    1166 
    +--
    1167 
    +-- You can get "deep" by supplying a predicate that also looks in the kind
    1166 1168 
     afvFolder = TyCoFolder { tcf_view = noView  -- See Note [Free vars and synonyms]
    1167 1169 
                            , tcf_tyvar = do_tcv
    1168 1170 
                            , tcf_covar = do_tcv
    ... ... @@ -1173,8 +1175,7 @@ afvFolder = TyCoFolder { tcf_view = noView -- See Note [Free vars and synonyms]
    1173 1175 
         -- Check the variable itself with check_fv,
    1174 1176 
         -- and check its kind (this is a deep folder)
    1175 1177 
         do_tcv tcv = MkFV $ \ (bvs,check_fv) ->
    1176 
    -                 Any (not (tcv `elemVarSet` bvs) &&
    1177 
    -                      (check_fv tcv || runAny check_fv (afv_type (varType tcv))))
    1178 
    +                 Any (not (tcv `elemVarSet` bvs) && check_fv tcv)
    1178 1179 
         do_hole hole = do_tcv (coHoleCoVar hole)
    1179 1180
    1180 1181 
     afv_type  :: Type     -> FV (BoundVars, TyVar -> Bool) DM.Any
    ... ... @@ -1186,16 +1187,32 @@ runAny :: (TyVar -> Bool) -> FV (BoundVars, TyCoVar -> Bool) DM.Any -> Bool
    1186 1187 
     {-# INLINE runAny #-}
    1187 1188 
     runAny check_fv fvs = DM.getAny (runFV fvs (emptyVarSet, check_fv))
    1188 1189
    1190 
    +---------------------------------------------
    1191 
    +-- anyShallowFreeVarsOfType and friends look only for shallow free vars
    1192 
    +--    (Currently not needed, left here in case we need it one day)
    1193 
    +-- anyShallowFreeVarsOfType :: (TyCoVar -> Bool) -> Type -> Bool
    1194 
    +-- {-# INLINE anyShallowFreeVarsOfType #-}
    1195 
    +-- anyShallowFreeVarsOfType check_fv ty = runAny check_fv (afv_type ty)
    1196 
    +
    1197 
    +---------------------------------------------
    1198 
    +-- anyFreeVarsOfType and friends look for deep free vars
    1199 
    +
    1200 
    +deep_check :: (TyCoVar -> Bool) -> TyCoVar -> Bool
    1201 
    +-- This is inefficient because if one tyvar occurs many times
    1202 
    +-- in a type, it'll look in its kind at each occurrence. Boo.
    1203 
    +deep_check check_fv tcv = check_fv tcv || anyFreeVarsOfType check_fv (varType tcv)
    1204 
    +
    1189 1205 
     anyFreeVarsOfType :: (TyCoVar -> Bool) -> Type -> Bool
    1190 1206 
     {-# INLINE anyFreeVarsOfType #-}
    1191 
    -anyFreeVarsOfType check_fv ty = runAny check_fv (afv_type ty)
    1207 
    +-- Looks deeply, into the kinds of the free vars
    1208 
    +anyFreeVarsOfType check_fv ty = runAny (deep_check check_fv) (afv_type ty)
    1192 1209
    1193 1210 
     anyFreeVarsOfTypes :: (TyCoVar -> Bool) -> [Type] -> Bool
    1194 1211 
     {-# INLINE anyFreeVarsOfTypes #-}
    1195 
    -anyFreeVarsOfTypes check_fv tys = runAny check_fv (afv_types tys)
    1212 
    +anyFreeVarsOfTypes check_fv tys = runAny (deep_check check_fv) (afv_types tys)
    1196 1213
    1197 1214 
     anyFreeVarsOfCo :: (TyCoVar -> Bool) -> Coercion -> Bool
    1198 
    -anyFreeVarsOfCo check_fv co = runAny check_fv (afv_co co)
    1215 
    +anyFreeVarsOfCo check_fv co = runAny (deep_check check_fv) (afv_co co)
    1199 1216
    1200 1217 
     noFreeVarsOfType :: Type -> Bool
    1201 1218 
     noFreeVarsOfType ty = not $ runAny (const True) (afv_type ty)
    ... ... @@ -1206,6 +1223,7 @@ noFreeVarsOfTypes tys = not $ runAny (const True) (afv_types tys)
    1206 1223 
     noFreeVarsOfCo :: Coercion -> Bool
    1207 1224 
     noFreeVarsOfCo co = not $ runAny (const True) (afv_co co)
    1208 1225
    1226 
    +
    1209 1227 
     {-
    1210 1228 
     ************************************************************************
    1211 1229 
     *                                                                      *

  • compiler/GHC/Core/TyCo/Subst.hs
    ... ... @@ -48,6 +48,8 @@ module GHC.Core.TyCo.Subst
    48 48 
             substTyCoBndr,
    49 49 
             substVarBndrUsing,
    50 50 
             checkValidSubst, isValidTCvSubst,
    51 
    +
    52 
    +        deepSubstTy
    51 53 
       ) where
    52 54
    53 55 
     import GHC.Prelude
    ... ... @@ -775,9 +777,15 @@ substThetaUnchecked = substTysUnchecked
    775 777 
     -- building no thunks.  See Note [Specialising mappers] in GHC.Core.TyCo.Make
    776 778 
     type SubstM = StrictReaderT Subst StrictIdentity
    777 779
    778 
    -runSubstM :: SubstM a -> Subst -> a
    779 
    -runSubstM m subst = runStrictIdentity (runStrictReaderT m subst)
    780 
    +runSubstM :: forall a. (a -> SubstM a) -> Subst -> a -> a
    780 781 
     {-# INLINE runSubstM #-}
    782 
    +runSubstM tx subst x = runStrictIdentity (runStrictReaderT (tx x) subst)
    783 
    +
    784 
    +subst_ty :: Subst -> Type -> Type
    785 
    +subst_co :: Subst -> Coercion -> Coercion
    786 
    +(subst_ty, subst_co)
    787 
    +  = case mapTyCo substTyCoMapper of
    788 
    +      (ms_ty, _, ms_co, _) -> (runSubstM ms_ty, runSubstM ms_co)
    781 789
    782 790 
     substTyCoMapper :: TyCoMapper SubstM
    783 791 
     substTyCoMapper
    ... ... @@ -785,8 +793,8 @@ substTyCoMapper
    785 793 
                    , tcm_covar      = subst_cv
    786 794 
                    , tcm_hole       = subst_ch
    787 795 
                    , tcm_tycobinder = tcv_bndr
    788 
    -               , tcm_tcapp_ty   = tcapp_ty
    789 
    -               , tcm_tcapp_co   = tcapp_co
    796 
    +               , tcm_tcapp_ty   = nopTcAppTy
    797 
    +               , tcm_tcapp_co   = nopTcAppCo
    790 798 
                    }
    791 799 
      where
    792 800 
        subst_tv tv = StrictReaderT $ \subst -> return (substTyVar  subst tv)
    ... ... @@ -802,23 +810,15 @@ substTyCoMapper
    802 810
    803 811 
        -- Avoid allocation in this very
    804 812 
        -- common case (E.g. Int, LiftedRep etc)
    805 
    -   tcapp_ty :: Type -> TyCon -> [Type] -> SubstM Type
    806 
    -   tcapp_ty ty tc tys'
    807 
    -      | null tys'  = return ty
    808 
    -      | otherwise  = return (mkTyConApp tc tys')
    809 
    -   tcapp_co :: Coercion -> Role -> TyCon -> [Coercion] -> SubstM Coercion
    810 
    -   tcapp_co co r tc cos'
    811 
    -      | null cos'  = return co
    812 
    -      | otherwise  = return (mkTyConAppCo r tc cos')
    813 
    +nopTcAppTy :: Type -> TyCon -> [Type] -> SubstM Type
    814 
    +nopTcAppTy  ty tc tys'
    815 
    +  | null tys'  = return ty
    816 
    +  | otherwise  = return (mkTyConApp tc tys')
    813 817
    814 
    -subst_ty :: Subst -> Type -> Type
    815 
    -subst_co :: Subst -> Coercion -> Coercion
    816 
    -(subst_ty, subst_co)
    817 
    -  = case mapTyCo substTyCoMapper of
    818 
    -      (ms_ty, _, ms_co, _) -> (run ms_ty, run ms_co)
    819 
    -  where
    820 
    -    run :: forall a. (a -> SubstM a) -> Subst -> a -> a
    821 
    -    run ms subst x = runSubstM (ms x) subst
    818 
    +nopTcAppCo :: Coercion -> Role -> TyCon -> [Coercion] -> SubstM Coercion
    819 
    +nopTcAppCo co r tc cos'
    820 
    +  | null cos'  = return co
    821 
    +  | otherwise  = return (mkTyConAppCo r tc cos')
    822 822
    823 823 
     substTyVar :: Subst -> TyVar -> Type
    824 824 
     substTyVar (Subst _ _ tenv _) tv
    ... ... @@ -1019,3 +1019,86 @@ it is /very/ valuable to /keep/ it empty:
    1019 1019 
       If the substitution is empty, this is a no-op -- but only if it
    1020 1020 
       is empty!
    1021 1021 
     -}
    1022 
    +
    1023 
    +
    1024 
    +{- **********************************************************************
    1025 
    +%*                                                                      *
    1026 
    +                Deep substitution
    1027 
    +%*                                                                      *
    1028 
    +%********************************************************************* -}
    1029 
    +
    1030 
    +{- Note [Deep substitution]
    1031 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~
    1032 
    +Deep substitution applies the substitution to the /kinds/ of un-substituted
    1033 
    +type variables.  Suppose the substitution is
    1034 
    +    [ k :-> Type ]
    1035 
    +and we apply it to the type
    1036 
    +    Proxy k (a :: k)
    1037 
    +Ordinary shallow substitution will give
    1038 
    +    Proxy Type (a :: k)
    1039 
    +which is ill-kinded.  Deep substitution will give
    1040 
    +    Proxy Type (a :: Type)
    1041 
    +
    1042 
    +Ordinary (shallow) substitution is usually fine, because we will substitute for
    1043 
    +`a` as well, but not always.  In particular, the pure unifier in GHC.Core.Unify
    1044 
    +uses `niFixSubst` to find a fixpoint, and we really don't want domain tyvars
    1045 
    +appearing in the range.  See Note [Finding the substitution fixpoint].
    1046 
    +
    1047 
    +Wrinkles:
    1048 
    +
    1049 
    +(DS1) Deep substitution risks being rather inefficient because it re-applies the
    1050 
    +  substitution to the kind at /each occurrence/ of a free variable.  We could
    1051 
    +  perhaps find the free vars, and build a re-kinding substitution, but that's a
    1052 
    +  bit more complicated.
    1053 
    +
    1054 
    +(DS2) Deep substitution, as implemented here, relies on invariant
    1055 
    +  (NoTypeShadowing); see Note [No type-shadowing in Core] in Core.hs.
    1056 
    +  Otherwise we may have e.g.
    1057 
    +     S = [r :-> LiftedRep]   in-scope = {r, x}
    1058 
    +     T = forall (r :: RuntimeRep). (x :: TYPE r) -> ...
    1059 
    +  and we would want to apply the outer substitution S to the
    1060 
    +  occurrence of r in the kind of x.  But we'll have removed it
    1061 
    +  from the subsitution when pasing the 'forall r'.
    1062 
    +-}
    1063 
    +
    1064 
    +deepSubstTyCoMapper :: TyCoMapper SubstM
    1065 
    +deepSubstTyCoMapper
    1066 
    +  = TyCoMapper { tcm_tyvar      = subst_tv
    1067 
    +               , tcm_covar      = subst_cv
    1068 
    +               , tcm_hole       = subst_ch
    1069 
    +               , tcm_tycobinder = tcv_bndr
    1070 
    +               , tcm_tcapp_ty   = nopTcAppTy
    1071 
    +               , tcm_tcapp_co   = nopTcAppCo
    1072 
    +               }
    1073 
    + where
    1074 
    +   subst_tv tv = StrictReaderT $ \subst -> return (deepSubstTyVar  subst tv)
    1075 
    +   subst_cv cv = StrictReaderT $ \subst -> return (deepSubstCoVar  subst cv)
    1076 
    +   subst_ch ch = StrictReaderT $ \subst -> return (deepSubstCoHole subst ch)
    1077 
    +
    1078 
    +   tcv_bndr :: TyCoVar -> ForAllTyFlag -> (TyCoVar -> SubstM r) -> SubstM r
    1079 
    +   tcv_bndr tcv _vis k
    1080 
    +     = StrictReaderT $ \subst ->
    1081 
    +       let !(subst', tcv') = substVarBndrUsing deepSubstTy subst tcv
    1082 
    +       in runStrictReaderT (k tcv') subst'
    1083 
    +
    1084 
    +deepSubstTy :: Subst -> Type -> Type
    1085 
    +deepSubstTy = case mapTyCo deepSubstTyCoMapper of
    1086 
    +                (subst_ty, _, _, _) -> runSubstM subst_ty
    1087 
    +
    1088 
    +deepSubstTyVar :: Subst -> TyVar -> Type
    1089 
    +deepSubstTyVar subst@(Subst _ _ tenv _) tv
    1090 
    +  = assert (isTyVar tv) $
    1091 
    +    case lookupVarEnv tenv tv of
    1092 
    +      Just ty -> ty
    1093 
    +      Nothing -> TyVarTy (updateVarType (deepSubstTy subst) tv)
    1094 
    +
    1095 
    +deepSubstCoVar :: Subst -> CoVar -> Coercion
    1096 
    +deepSubstCoVar subst@(Subst _ _ _ cenv) cv
    1097 
    +  = case lookupVarEnv cenv cv of
    1098 
    +      Just co -> co
    1099 
    +      Nothing -> CoVarCo (updateVarType (deepSubstTy subst) cv)
    1100 
    +
    1101 
    +deepSubstCoHole :: Subst -> CoercionHole -> Coercion
    1102 
    +-- See Note [Substituting in a coercion hole]
    1103 
    +deepSubstCoHole subst h@(CH { ch_co_var = cv })
    1104 
    +  = HoleCo (h { ch_co_var = updateVarType (deepSubstTy subst) cv })

  • compiler/GHC/Core/Type.hs
    ... ... @@ -483,7 +483,7 @@ expandTypeSynonyms ty
    483 483 
     expandTypeSynonymsX :: Subst -> Type -> Type
    484 484 
     expandTypeSynonymsX
    485 485 
       = case mapTyCo expandTypeSynonymMapper of
    486 
    -      (exp_ty, _, _, _) -> \subst ty -> runSubstM (exp_ty ty) subst
    486 
    +      (exp_ty, _, _, _) -> runSubstM exp_ty
    487 487
    488 488 
     expandTypeSynonymMapper :: TyCoMapper SubstM
    489 489 
     -- Just like substitution, but treat TyConApp specially

  • compiler/GHC/Core/Unify.hs
    ... ... @@ -28,13 +28,12 @@ import GHC.Types.Var.Env
    28 28 
     import GHC.Types.Var.Set
    29 29 
     import GHC.Core.Type     hiding ( getTvSubstEnv )
    30 30 
     import GHC.Core.Coercion hiding ( getCvSubstEnv )
    31 
    -import GHC.Core.Predicate( scopedSort )
    32 31 
     import GHC.Core.TyCon
    33 32 
     import GHC.Core.Predicate( CanEqLHS(..), canEqLHS_maybe )
    34 33 
     import GHC.Core.TyCon.Env
    35 34 
     import GHC.Core.TyCo.Rep
    36 35 
     import GHC.Core.TyCo.Compare ( eqType, tcEqType, tcEqTyConAppArgs )
    37 
    -import GHC.Core.TyCo.Subst   ( mkTvSubst )
    36 
    +import GHC.Core.TyCo.Subst   ( mkTvSubst, deepSubstTy )
    38 37 
     import GHC.Core.Map.Type
    39 38 
     import GHC.Core.Multiplicity
    40 39
    ... ... @@ -1063,21 +1062,31 @@ During unification we use a TvSubstEnv/CvSubstEnv pair that is
    1063 1062
    1064 1063 
     Note [Finding the substitution fixpoint]
    1065 1064 
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    1066 
    -Finding the fixpoint of a non-idempotent substitution arising from a
    1067 
    -unification is much trickier than it looks, because of kinds.  Consider
    1065 
    +We want an /idempotent/ substitution, so `niFixSubst` takes a non-idempotent
    1066 
    +one and composes it with itself until it becomes idempotent.  Thus if the original
    1067 
    +is S0, we compute S1 = S0 o S0, S2 = S1 o S1, etc.
    1068 
    +
    1069 
    +A variable chain v0 :-> v1 :-> ... :-> vm therefore takes about log2(m) rounds,
    1070 
    +The unifier can build such chains. For example:
    1071 
    +    (a, a, a, ..., a)   ~   (x1, x2, x3, ..., xm)
    1072 
    +produces a :-> x1, x1 :-> x2, ..., x(m-1) :-> xm.
    1073 
    +
    1074 
    +Finding the fixpoint is much trickier than it looks, because of kinds.
    1075 
    +Consider
    1068 1076 
        T k (H k (f:k)) ~ T * (g:*)
    1069 1077 
     If we unify, we get the substitution
    1070 1078 
        [ k -> *
    1071 1079 
        , g -> H k (f:k) ]
    1080 
    +This isn't idempotent: it mentions `k` in the range.
    1081 
    +
    1072 1082 
     To make it idempotent we don't want to get just
    1073 1083 
        [ k -> *
    1074 1084 
        , g -> H * (f:k) ]
    1075 
    -We also want to substitute inside f's kind, to get
    1076 
    -   [ k -> *
    1077 
    -   , g -> H k (f:*) ]
    1078 
    -If we don't do this, we may apply the substitution to something,
    1079 
    -and get an ill-formed type, i.e. one where typeKind will fail.
    1085 
    +because (H * (f:k)) is itself ill-kinded, and `typeKind` will fail.
    1080 1086 
     This happened, for example, in #9106.
    1087 
    +So (yuckily) we must also substitute inside f's kind, to get
    1088 
    +   [ k -> *
    1089 
    +   , g -> H * (f:*) ]
    1081 1090
    1082 1091 
     It gets worse.  In #14164 we wanted to take the fixpoint of
    1083 1092 
     this substitution
    ... ... @@ -1090,84 +1099,53 @@ the invocation of F! We don't have a function that recursively
    1090 1099 
     applies substitutions inside the kinds of variable occurrences (and
    1091 1100 
     probably rightly so).
    1092 1101
    1093 
    -So, we work as follows:
    1094 
    -
    1095 
    - 1. Start with the current substitution (which we are
    1096 
    -    trying to fixpoint
    1097 
    -       [ xs :-> F a (z :: a) (rest :: G a (z :: a))
    1098 
    -       , a  :-> b ]
    1099 
    -
    1100 
    - 2. Take all the free vars of the range of the substitution:
    1101 
    -       {a, z, rest, b}
    1102 
    -    NB: the free variable finder closes over
    1103 
    -        the kinds of variable occurrences
    1104 
    -
    1105 
    - 3. If none are in the domain of the substitution, stop.
    1106 
    -    We have found a fixpoint.
    1107 
    -
    1108 
    - 4. Remove the variables that are bound by the substitution, leaving
    1109 
    -       {z, rest, b}
    1110 
    -
    1111 
    - 5. Do a topo-sort to put them in dependency order:
    1112 
    -       [ b :: *, z :: a, rest :: G a z ]
    1113 
    -
    1114 
    - 6. Apply the substitution left-to-right to the kinds of these
    1115 
    -    tyvars, extending it each time with a new binding, so we
    1116 
    -    finish up with
    1117 
    -       [ xs   :-> ..as before..
    1118 
    -       , a    :-> b
    1119 
    -       , b    :-> b    :: *
    1120 
    -       , z    :-> z    :: b
    1121 
    -       , rest :-> rest :: G b (z :: b) ]
    1122 
    -    Note that rest now has the right kind
    1123 
    -
    1124 
    - 7. Apply this extended substitution (once) to the range of the
    1125 
    -    /original/ substitution.  (Note that the extended substitution
    1126 
    -    would go on forever if you tried to find its fixpoint, because it
    1127 
    -    maps z to z.)
    1128 
    -
    1129 
    - 8. And go back to step 1
    1130 
    -
    1131 
    -In Step 6 we use the free vars from Step 2 as the initial
    1132 
    -in-scope set, because all of those variables appear in the
    1133 
    -range of the substitution, so they must all be in the in-scope
    1134 
    -set.  But NB that the type substitution engine does not look up
    1135 
    -variables in the in-scope set; it is used only to ensure no
    1136 
    -shadowing.
    1102 
    +Ugh!  This whole thing is pretty horrible. But the solution is simple enough:
    1103 
    +
    1104 
    +        Use deep substitution (deepSubstTy)
    1105 
    +
    1106 
    +(deepSubst `s` (Proxy k (a::k)) applies the substitution `s` not only to
    1107 
    +the occurrence of `k` in the argument of `Proxy`, but also to the `k` inside
    1108 
    +the kind of `a`.  See Note [Deep substitution] in GHC.Core.TyCo.Subst.
    1109 
    +
    1110 
    +So `niFixSubst` just applies the substitution /deeply/ to the types in its
    1111 
    +range, until we reach a fixed point.  Easy!
    1112 
    +
    1113 
    +Historical Note:
    1114 
    +  Immediately prior to this solution there was a previous, more complicated
    1115 
    +  `niFixSubst` which involved finding the (deep) free variables and "re-kinding"
    1116 
    +  them.  It accomplished essentially the same things, and it avoided the
    1117 
    +  potential duplication noted in Note [Deep substitution].  But it was pretty
    1118 
    +  subtle and this version is more obviously correct.
    1119 
    +End of Historical Note
    1137 1120 
     -}
    1138 1121
    1139 1122 
     niFixSubst :: InScopeSet -> TvSubstEnv -> Subst
    1140 1123 
     -- Find the idempotent fixed point of the non-idempotent substitution
    1141 1124 
     -- This is surprisingly tricky:
    1142 1125 
     --   see Note [Finding the substitution fixpoint]
    1143 
    --- ToDo: use laziness instead of iteration?
    1144 1126 
     niFixSubst in_scope tenv
    1145 
    -  | not_fixpoint = niFixSubst in_scope (mapVarEnv (substTy subst) tenv)
    1146 
    -  | otherwise    = tenv_subst
    1127 
    +  | isEmptyVarEnv tenv     -- Fast path for common case
    1128 
    +  = mkEmptySubst in_scope
    1129 
    +  | otherwise
    1130 
    +  =  -- pprTrace "niFixSubst" (vcat [ text "In: " <+> ppr tenv
    1131 
    +     --                             , text "Out:" <+> ppr (S.getTvSubstEnv subst) ])
    1132 
    +     subst
    1147 1133 
       where
    1148 
    -    tenv_subst = mkTvSubst in_scope tenv   -- This is our starting point
    1149 
    -
    1150 
    -    range_tvs :: [TyVar]
    1151 
    -    range_tvs = nonDetVarSetElems $
    1152 
    -                tyCoVarsOfTypes $
    1153 
    -                nonDetEltsUFM tenv
    1154 
    -          -- It's OK to use nonDetEltsUFM (twice) here because
    1155 
    -          -- the order of range_tvs is immaterial
    1156 
    -
    1157 
    -    not_fixpoint  = any in_domain range_tvs
    1158 
    -    in_domain tv  = tv `elemVarEnv` tenv
    1134 
    +     subst = niFixSubst' 1 in_scope tenv
    1159 1135
    1160 
    -    free_tvs = scopedSort (filterOut in_domain range_tvs)
    1161 
    -
    1162 
    -    -- See Note [Finding the substitution fixpoint], Step 6
    1163 
    -    subst = foldl' add_free_tv tenv_subst free_tvs
    1164 
    -
    1165 
    -    add_free_tv :: Subst -> TyVar -> Subst
    1166 
    -    add_free_tv subst tv
    1167 
    -      | isTyVar tv = extendTvSubst subst tv (mkTyVarTy tv')
    1168 
    -      | otherwise  = subst  -- Ignore free coercion variables
    1169 
    -     where
    1170 
    -        tv' = updateTyVarKind (substTy subst) tv
    1136 
    +niFixSubst' :: Int -> InScopeSet -> TvSubstEnv -> Subst
    1137 
    +niFixSubst' n in_scope tenv_orig
    1138 
    +  | fixpoint_found = mkTvSubst in_scope tenv_orig
    1139 
    +  | otherwise      = niFixSubst' (n+1) in_scope tenv_new
    1140 
    +  where
    1141 
    +    in_dom tv = tv `elemVarEnv` tenv_orig
    1142 
    +    tenv_new  = mapVarEnv (deepSubstTy subst) tenv_orig
    1143 
    +    subst     = mkTvSubst in_scope tenv_orig
    1144 
    +
    1145 
    +    fixpoint_found = nonDetStrictFoldUFM and_fix True tenv_orig
    1146 
    +    and_fix :: Type -> Bool -> Bool
    1147 
    +    and_fix _ False = False
    1148 
    +    and_fix ty _    = not (anyFreeVarsOfType in_dom ty)
    1171 1149
    1172 1150 
     {-
    1173 1151 
     ************************************************************************

  • compiler/GHC/Tc/Instance/Family.hs
    ... ... @@ -16,6 +16,7 @@ import GHC.Prelude
    16 16 
     import GHC.Driver.DynFlags
    17 17 
     import GHC.Driver.Env
    18 18
    19 
    +import GHC.Core.Predicate( saturatedFamApp_maybe )
    19 20 
     import GHC.Core.FamInstEnv
    20 21 
     import GHC.Core.Coercion
    21 22 
     import GHC.Core.TyCon
    ... ... @@ -715,15 +716,9 @@ reportInjectivityErrors dflags fi_ax axiom inj
    715 716 
            when wrong_bare_rhs $ reportBareVariableInRHSErr   fam_tc bare_variables axiom
    716 717
    717 718 
     -- | Is type headed by a type family application?
    718 
    -isTFHeaded :: Type -> Bool
    719 719 
     -- See Note [Verifying injectivity annotation], case 3.
    720 
    -isTFHeaded ty | Just ty' <- coreView ty
    721 
    -              = isTFHeaded ty'
    722 
    -isTFHeaded ty | (TyConApp tc args) <- ty
    723 
    -              , isTypeFamilyTyCon tc
    724 
    -              = args `lengthIs` tyConArity tc
    725 
    -isTFHeaded _  = False
    726 
    -
    720 
    +isTFHeaded :: Type -> Bool
    721 
    +isTFHeaded ty = isJust (saturatedFamApp_maybe ty)
    727 722
    728 723 
     -- | If a RHS is a bare type variable return a set of LHS patterns that are not
    729 724 
     -- bare type variables.

  • compiler/GHC/Tc/Solver/FunDeps.hs
    ... ... @@ -24,16 +24,16 @@ import GHC.Tc.Types.Constraint
    24 24 
     import GHC.Core.FamInstEnv
    25 25 
     import GHC.Core.Coercion
    26 26 
     import GHC.Core.TyCo.Rep( Type(..) )
    27 
    -import GHC.Core.Predicate( EqRel(..) )
    27 
    +import GHC.Core.TyCo.Subst( deepSubstTy, elemSubst, extendTvSubstWithClone )
    28 
    +import GHC.Core.Predicate( EqRel(..), saturatedFamApp_maybe )
    28 29 
     import GHC.Core.TyCon
    29 30 
     import GHC.Core.Unify( AmIUnifying(..)
    30 31 
                          , tcUnifyTysForInjectivity, typeListsAreApart )
    31 32 
     import GHC.Core.Coercion.Axiom
    32 
    -import GHC.Core.TyCo.Subst( elemSubst, extendTvSubstWithClone )
    33 33
    34 34 
     import GHC.Builtin.WiredIn.TypeLits( tryInteractTopFam, tryInteractInertFam )
    35 35
    36 
    -import GHC.Types.Var( TyVar, tyVarKind, setTyVarKind )
    36 
    +import GHC.Types.Var( TyVar, updateVarType, tyVarKind )
    37 37 
     import GHC.Types.Var.Set
    38 38 
     import GHC.Types.Var.Env( mkInScopeSet )
    39 39
    ... ... @@ -57,7 +57,6 @@ Here is our plan for dealing with functional dependencies
    57 57 
            * send the current constraint back to the start of the pipeline;
    58 58 
              it might now be soluble, and it probably isn't inert
    59 59
    60 
    -
    61 60 
     * Once a unification is done, it can't be un-done.  So we must be very careful
    62 61 
       not to threaten completeness by doing a unification when there might be
    63 62 
       another way to solve the constraint.
    ... ... @@ -613,6 +612,7 @@ tryFamEqFunDeps mode eqs_for_me fam_tc work_args
    613 612
    614 613 
     mkTopFamEqFDs :: TyCon -> [TcType] -> EqCt -> SolverStage [FunDepEqns]
    615 614 
     mkTopFamEqFDs fam_tc work_args work_item
    615 
    +  -- NB: work_args exactly saturate fam_tc
    616 616 
       | isOpenTypeFamilyTyCon fam_tc
    617 617 
       , Injective inj_flags <- tyConInjectivityInfo fam_tc
    618 618 
       = -- Open, injective type families
    ... ... @@ -694,6 +694,8 @@ hasRelevantGiven eqs_for_me work_args (EqCt { eq_rhs = work_rhs })
    694 694 
     getRelevantBranches :: CoAxiom Branched -> [TcType] -> Xi -> [FunDepEqns]
    695 695 
     -- Return the FunDepEqns that arise from each relevant branch
    696 696 
     -- Implements Note [Relevance]
    697 
    +-- Caller will only use these FunDepEqns if there is just one relevant
    698 
    +-- equation, i.e. the returned [FunDepEqns] is a singleton.
    697 699 
     getRelevantBranches ax work_args work_rhs
    698 700 
       = go (fromBranches (coAxiomBranches ax))
    699 701 
       where
    ... ... @@ -709,24 +711,33 @@ getRelevantBranches ax work_args work_rhs
    709 711 
                                             , cab_lhs = lhs_tys
    710 712 
                                             , cab_rhs = rhs_ty })
    711 713 
                 | Just subst <- tcUnifyTysForInjectivity Unifying (rhs_ty:lhs_tys) work_tys
    712 
    -              -- See (RW1)-(RW3) in Note [Relevance]
    713 
    -              -- This is a pre-/unification/ check (not matching)
    714 
    -              -- so `subst` can bind both `qtvs` and fvs(work_tys)
    715 
    -            , let (subst',qtvs') = trim_qtvs subst qtvs
    716 
    -                  lhs_tys'       = substTys subst' lhs_tys
    717 
    -                  rhs_ty'        = substTy  subst' rhs_ty
    718 
    -                  branch_tys'    = rhs_ty' : lhs_tys'
    714 
    +                            -- See (RW1)-(RW3) in Note [Relevance]
    715 
    +            , let lhs_tys' = map (deepSubstTy subst) lhs_tys
    716 
    +                  -- deepSubstTy: see (CF8) in Note [Exploiting closed type families]
    719 717 
                 , noEarlierMatchCheck lhs_tys' branch  -- See (RW4) in Note [Relevance]
    720 
    -            = Just (FDEqns { fd_qtvs = qtvs'
    721 
    -                           , fd_eqs  = zipWith Pair branch_tys' work_tys })
    722 
    -                              -- Do not apply the substition to `work_tys`;
    723 
    -                              -- See (CF7) in Note [Exploiting closed type families]
    718 
    +            = -- Ignore the substitution, except for `noEarlierMatchCheck`
    719 
    +              Just $
    720 
    +              if all (`elemSubst` subst) qtvs
    721 
    +              then -- `subst` eliminates all qtvs; and no qtvs in range of subst
    722 
    +                   -- See (CF7)(A) in Note [Exploiting closed type families]
    723 
    +                   FDEqns { fd_qtvs = []
    724 
    +                          , fd_eqs  = zipWith Pair (substTy subst rhs_ty : lhs_tys')
    725 
    +                                                   work_tys }
    726 
    +                          -- Do not apply `subst` to `work_tys`;
    727 
    +                          -- See (CF9) in Note [Exploiting closed type families]
    728 
    +
    729 
    +              else -- Abandon `subst`; re-create it from (rhs_ty ~ work_rhs)
    730 
    +                   -- See (CF7)(B) in Note [Exploiting closed type families]
    731 
    +                   FDEqns { fd_qtvs = qtvs
    732 
    +                          , fd_eqs  = zipWith Pair (rhs_ty:lhs_tys) work_tys }
    733 
    +
    724 734 
                 | otherwise
    725 735 
                 = Nothing
    726 736
    727 737 
     mkTopOpenFamEqFDs :: TyCon -> [Bool] -> [TcType] -> EqCt -> TcS [FunDepEqns]
    728 738 
     -- Implements (INJFAM:Wanted/top-open)
    729 739 
     -- See Note [Exploiting open type families]
    740 
    +-- NB: work_args exactly saturate fam_tc
    730 741 
     mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs })
    731 742 
       = do { fam_envs <- getFamInstEnvs
    732 743 
            ; let branches :: [CoAxBranch]
    ... ... @@ -739,11 +750,14 @@ mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs })
    739 750 
                            , cab_lhs = branch_lhs_tys
    740 751 
                            , cab_rhs = branch_rhs })
    741 752 
           | Just subst <- tcUnifyTysForInjectivity Matching [branch_rhs] [work_rhs]
    742 
    -      , let (subst', qtvs') = trim_qtvs subst branch_qtvs
    753 
    +        -- No need for an apartness check here;
    754 
    +        -- for open type families there are no "preceding" equations
    755 
    +        -- Both branch_lhs_tys and work_args exactly saturate fam_tc
    756 
    +      , let (subst', qtvs') = trimQtvs subst branch_qtvs
    743 757 
                 branch_lhs_tys' = substTys subst' branch_lhs_tys
    744 
    -        -- No need for an apartness check here; for open type families
    745 
    -        -- there are no "preceding" equations
    746 
    -      = Just (mkInjectivityFDEqn inj_flags qtvs' branch_lhs_tys' work_args)
    758 
    +        -- We must apply the substitution here see
    759 
    +        -- the Basic Plan in Note [Exploiting open type families]
    760 
    +      = Just (mkInjectivityFDEqn qtvs' inj_flags branch_lhs_tys' work_args)
    747 761
    748 762 
           | otherwise
    749 763 
           = Nothing
    ... ... @@ -756,9 +770,9 @@ mkLocalFamEqFDs eqs_for_me fam_tc inj_flags work_args work_rhs
    756 770 
       = do { let -- eqns_from_inerts: see (INJFAM:Wanted/other)
    757 771 
                  eqns_from_inerts = mapMaybe do_one eqs_for_me
    758 772 
                  -- eqns_from_self: see (INJFAM:Wanted/Self)
    759 
    -             eqns_from_self   = case tcSplitTyConApp_maybe work_rhs of
    760 
    -                                  Just (tc,rhs_tys) | tc==fam_tc -> [mk_eqn rhs_tys]
    761 
    -                                  _                              -> []
    773 
    +             eqns_from_self = case saturatedFamApp_maybe work_rhs of
    774 
    +                                Just (tc, rhs_tys) | fam_tc == tc -> [mk_eqn rhs_tys]
    775 
    +                                _                                 -> []
    762 776
    763 777 
            ; return (eqns_from_inerts ++ eqns_from_self) }
    764 778 
       where
    ... ... @@ -768,11 +782,12 @@ mkLocalFamEqFDs eqs_for_me fam_tc inj_flags work_args work_rhs
    768 782 
           | otherwise                     = Nothing
    769 783 
         do_one _ = pprPanic "interactFunEq 2" (ppr fam_tc)  -- TyVarLHS
    770 784
    771 
    -    mk_eqn iargs = mkInjectivityFDEqn inj_flags [] work_args iargs
    785 
    +    mk_eqn iargs = mkInjectivityFDEqn [] inj_flags work_args iargs
    786 
    +
    772 787
    773 
    -trim_qtvs :: Subst -> [TyVar] -> (Subst, [TyVar])
    774 
    --- Tricky stuff: see (OF1) in Note [Exploiting open type families]
    775 
    -trim_qtvs unif_subst qtvs
    788 
    +trimQtvs :: Subst -> [TyVar] -> (Subst, [TyVar])
    789 
    +-- Tricky stuff: see Note [Exploiting open type families] and Note [trimQtvs]
    790 
    +trimQtvs unif_subst qtvs
    776 791 
       = go unif_subst qtvs
    777 792 
       where
    778 793 
         go :: Subst -> [TyVar] -> (Subst, [TyVar])
    ... ... @@ -786,10 +801,9 @@ trim_qtvs unif_subst qtvs
    786 801 
         go_fresh subst tv tvs = (subst'', tv':tvs')
    787 802 
           where
    788 803 
             !(subst'', tvs') = go subst' tvs
    789 
    -        tv'    = tv `setTyVarKind` substTy subst (tyVarKind tv)
    804 
    +        tv'    = updateVarType (substTy subst) tv
    790 805 
             subst' = extendTvSubstWithClone subst tv tv'
    791 
    -                 -- extendTvSubstWithClone: see (OF1b) in
    792 
    -                 -- Note [Exploiting open type families]
    806 
    +                 -- extendTvSubstWithClone: see (TQ1) in Note [trimQtvs]
    793 807
    794 808
    795 809 
     -----------------------------------------
    ... ... @@ -883,15 +897,22 @@ mkLocalBuiltinFamEqFDs eqs_for_me fam_tc ops work_args work_rhs
    883 897 
            ; return (eqns_from_inerts ++ eqns_from_self) }
    884 898
    885 899 
     --------------------
    886 
    -mkInjectivityFDEqn :: [Bool]       -- Injectivity flags
    887 
    -                   -> [TcTyVar]    -- Quantify these
    900 
    +mkInjectivityFDEqn :: [TcTyVar]             -- Quantify these
    901 
    +                   -> [Bool]                -- Injectivity flags
    888 902 
                        -> [TcType] -> [TcType]  -- Make these equal
    889 903 
                        -> FunDepEqns
    890 904 
     -- When F s1 s2 s3 ~ F t1 t2 t3, and F has injectivity info [True,False,True]
    891 905 
     --   return the FDEqns { fd_eqs = [Pair s1 t1, Pair s3 t3] }
    892 
    --- The injectivity flags [Bool] will not all be False, but nothing goes wrong if they are
    893 
    -mkInjectivityFDEqn inj_args qtvs lhs_args rhs_args
    894 
    -  = FDEqns { fd_qtvs = qtvs, fd_eqs = eqs }
    906 
    +-- The injectivity flags [Bool] will not all be False,
    907 
    +--   but nothing goes wrong if they are
    908 
    +mkInjectivityFDEqn qtvs inj_args lhs_args rhs_args
    909 
    +  = assertPpr (let len = length inj_args in
    910 
    +               len == length lhs_args && len == length rhs_args)
    911 
    +              (vcat [ text "inj_args:" <+> ppr inj_args
    912 
    +                    , text "lhs_args:" <+> ppr lhs_args
    913 
    +                    , text "rhs_args:" <+> ppr rhs_args ]) $
    914 
    +    -- Need inj_args lhs_args and rhs_args to be same length for zip3
    915 
    +    FDEqns { fd_qtvs = qtvs, fd_eqs = eqs }
    895 916 
       where
    896 917 
         eqs = [ Pair lhs_arg rhs_arg
    897 918 
               | (True, lhs_arg, rhs_arg) <- zip3 inj_args lhs_args rhs_args ]
    ... ... @@ -1096,73 +1117,108 @@ Note [Exploiting closed type families].
    1096 1117
    1097 1118 
     Note [Exploiting open type families] see `mkTopOpenFamEqFDs`
    1098 1119 
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    1099 
    -Generating fundeps from a top-level type instance is covered in Section 5.2 in
    1100 
    -the Injective Type Families paper. For open type families, suppose we have
    1101 
    -
    1102 
    -   type family F a = r | r -> a
    1103 
    -   type instance F [a] = a->a
    1104 
    -
    1105 
    -   [W] F alpha ~ Int->Int
    1106 
    -
    1107 
    -Then, since F has been checked as injective, and the RHS `a->a` (pre-)unifies
    1108 
    -with the `Int->Int` in the Wanted with substitution [a :-> Int], we can
    1109 
    -add a derived FunDepEqns
    1120 
    +For an open type family, generating fundeps from a top-level type instance
    1121 
    +is covered in Section 5.2 in the Injective Type Families paper.
    1122 
    +
    1123 
    +Basic plan: Suppose type family F a b = r | r -> b
    1124 
    +            and Wanted [W] F wlhs1 wlhs2 ~ wrhs
    1125 
    +  Then for each type instance (F lhs1 lhs2 = rhs)
    1126 
    +  * Pre-match `rhs` against `wrhs` to get a substitution S
    1127 
    +  * Generate fundep equalities  S(lhs2) ~ wrhs
    1128 
    +    one for each fundep in the type family
    1129 
    +
    1130 
    +For example, suppose we have
    1131 
    +   type family F a b = r | r -> a
    1132 
    +   type instance F [a] Int = a->a
    1133 
    +   [W] F alpha beta ~ Int->Int
    1134 
    +Then we pre-match template (a->a) against target (Int->Int) to get
    1135 
    +substitution S = [a :-> Int].  Then we can generate
    1110 1136 
        FDEqns{ fd_qtvs = [], fd_eqs = [ [Int] ~ alpha ] }
    1111 1137 
     and thereby emit (via `instantiateFunDepEqns`)
    1112 1138 
        [W] [Int] ~ alpha
    1139 
    +Note that `fd_qtvs = []`; we have substituted away the quantifed type variable `a`.
    1113 1140
    1114 1141 
     Things are a bit trickier when not all the quantified variables of the
    1115 1142 
     instance are bound by the pre-unification step.  Suppose we have
    1116 
    -
    1117 1143 
        type family F a = r | r -> a
    1118 
    -   type instance F (Maybe a) = [G a]   -- G is a type family
    1144 
    +   type instance F (b -> Maybe a) = [(G a,b)]   -- G is a type family
    1145 
    +   [W] F alpha ~ [(ty,Int)]
    1119 1146
    1120 
    -   [W] F alpha ~ [ty]
    1121 
    -
    1122 
    -Then, the RHS [G a] pre-unifies with the RHS of the Wanted, but with an
    1123 
    -empty substitution, which does not fix `a`.  So we get this FunDepEqns:
    1124 
    -   FDEqns{ fd_qtvs = a, fd_eqs = [ Maybe a ~ alpha ] }
    1147 
    +Then, the RHS [(G a,b)] pre-matches with the RHS of the Wanted, but with
    1148 
    +the substitution [b :-> Int], which does not fix `a`.  So, after trimming
    1149 
    +the quantified type variables, we get this FunDepEqns:
    1150 
    +   FDEqns{ fd_qtvs = [a], fd_eqs = [ (Int -> Maybe a) ~ alpha ] }
    1125 1151 
     (note the fd_qtvs=a) and thereby emit (via `instantiateFunDepEqns`)
    1126 
    -   [W] Maybe gamma ~ alpha    -- Fresh gamma
    1127 
    -We have learned that `alpha` must be a list, but that is all; we don't
    1128 
    -know what is inside it, hence the fresh `gamma`.
    1129 
    -
    1130 
    -In general we have:
    1131 
    -
    1132 
    -  type family F x1 ... xn = r | r -> x1 x3     (say)
    1133 
    -  type instance forall qs. F t1 ... tn = rhs
    1134 
    -  [W] F a1 ... an ~ b
    1135 
    -
    1136 
    -Suppose `b` pre-unifies with `rhs`, with substitution `S` that binds
    1137 
    -some (but perhaps not all) of the `qs`.  Lets say
    1138 
    -   unbound_qs = qs \ dom(S)
    1139 
    -
    1140 
    -Then we generate the FunDepEqs
    1141 
    -   FDEqns{ fd_qtvs = unbound_qs
    1142 
    -         , fd_eqs = [ S(t1) ~ S(a1), S(t3) ~ S(a3) ]
    1143 
    -
    1144 
    -These 'fd_qtvs' are subsequently instantiated to fresh metavariables by
    1145 
    -'instantiateFunDepEqns'.
    1146 
    -
    1147 
    -(OF1) The computation of `unbound_qs` is done by `trim_qtvs`, but we
    1148 
    -   have to be careful.   Suppose (OF1a)
    1149 
    -       qs = [ k::*, a::k ]
    1150 
    -       S  = [ k :-> UnliftedType ]
    1151 
    -   Then we want
    1152 
    -       unbound_qs = [ a::UnliftedType ]    -- Must apply S to q's kind!!
    1153 
    -
    1154 
    -   And (OF1b), although I'm not sure if this can acutally happen:
    1155 
    -        qs = [ k::*, a::(k::*), b::(a::k) ]
    1156 
    -        S  = [ k :-> UnliftedType ]
    1157 
    -   We want
    1158 
    -        unbound_qs = [ a::UnliftedType, b::(a::UnliftedType) ]
    1159 
    -   Note that the occurrence of `a` in b's kind should be replaced by the
    1160 
    -   newly-kinded `a` not the original `a::k`.
    1161 
    -
    1162 
    -   This fancy footwork for `fd_qtvs` is done by `trim_qtvs`.  It
    1163 
    -    * Drops a quantified tyvar that /is/ matched
    1164 
    -    * Substitutes in the kind of a quantified tyvar `a` that is /not/ matched
    1165 
    -    * Adds the substitution [a::k :-> a::S(k)] to the substitution
    1152 
    +   [W] (Int -> Maybe gamma) ~ alpha    -- Fresh gamma
    1153 
    +We have learned that `alpha` must be a list of functions, but that is all;
    1154 
    +we don't know `gamma`.
    1155 
    +
    1156 
    +It gets tricker.  Suppose we have
    1157 
    +   type family F @k a = r | r -> k,a
    1158 
    +   type instance F @k (Proxy @k (a::k)) = T k
    1159 
    +   [W] F alpha beta ~ T Type
    1160 
    +Matching the RHS gives substitution [k :-> Type].   But we do /not/ want
    1161 
    +to end up with this:
    1162 
    +   FDEqns{ fd_qtvs = [a::k], fd_eqs = [ Proxy @Type (a::k) ~ alpha ] }
    1163 
    +because that `k`, hidden inside the kind of `a`, escapes into the solver.
    1164 
    +
    1165 
    +Instead we must not only "trim" the quantified variables of the equation,
    1166 
    +but /substitute/ in the kinds of the leftover quantified ones: see Note [trimQtvs].
    1167 
    +Then we get
    1168 
    +   FDEqns{ fd_qtvs = [a::Type], fd_eqs = [ Proxy @Type (a::Type) ~ alpha ] }
    1169 
    +
    1170 
    +Side note:
    1171 
    +
    1172 
    +You might wonder whether we can use the same solution as we do for /closed/
    1173 
    +families, by generating an equality for the RHSs; see (CF7).  But we can't.
    1174 
    +Example:
    1175 
    +   type family G a where G Int = Char
    1176 
    +   type family F a b = r | r -> a
    1177 
    +   type instance F a   [c]  = (a, G a)      -- (I1)
    1178 
    +   type instance F Int Bool = (Int, Bool)   -- (I2)
    1179 
    +   [W] F alpha Bool ~ (Int,gamma)
    1180 
    +Note that (I1) and (I2) are pariwise-injective: if the RHSs are the same,
    1181 
    +the LHSs are the same /in the injective position(s)/.  See Section 4.2 in
    1182 
    +the "Injective Type Families" paper.  We pre-match (I1) against the Wanted
    1183 
    +giving substitution  [a :-> Int].  We /cannot/ then generate
    1184 
    +   FDEqns { fd_qtvs = [a,c], fd_eqs = [ a~alpha
    1185 
    +                                      , (a,G a)~(Int,gamma) ] }
    1186 
    +where the second equality (wrongly)equates the RHSs.  This is wrong because we
    1187 
    +can solve those fundeps unifying alpha:=Int, gamma:=Char, by reducing (G a) to
    1188 
    +Char.  So we end up with [W] F Int Char, which is insoluble.  Bad.
    1189 
    +
    1190 
    +End of side note.
    1191 
    +
    1192 
    +Note [trimQtvs]
    1193 
    +~~~~~~~~~~~~~~~
    1194 
    +In Note [Exploiting open type families], we needed to "trim" the quantified
    1195 
    +type variables of the axiom, removing ones that are eliminated by the
    1196 
    +auubstitution `S`.  So can we just do this?
    1197 
    +     unbound_qs = qs \ dom(S)
    1198 
    +so that we could make fresh meta-variables for only the unbound `qs`.
    1199 
    +No, we can't. Suppose (TQ1)
    1200 
    +    qs = [ k::*, a::k ]
    1201 
    +    S  = [ k :-> UnliftedType ]
    1202 
    +Then we want
    1203 
    +    unbound_qs = [ a::UnliftedType ]    -- Must apply S to q's kind!!
    1204 
    +
    1205 
    +And (TQ2), although I'm not sure if this can actually happen:
    1206 
    +     qs = [ k::*, a::(k::*), b::(a::k) ]
    1207 
    +     S  = [ k :-> UnliftedType ]
    1208 
    +We want
    1209 
    +     unbound_qs = [ a::UnliftedType, b::(a::UnliftedType) ]
    1210 
    +Note that the occurrence of `a` in b's kind should be replaced by the
    1211 
    +newly-kinded `a` not the original `a::k`.
    1212 
    +
    1213 
    +The function `trimQtvs` does the job.  It
    1214 
    + * Drops a quantified tyvar that /is/ matched
    1215 
    + * Substitutes in the kind of a quantified tyvar `a` that is /not/ matched
    1216 
    + * Adds the substitution [a::k :-> a::S(k)] to the substitution
    1217 
    +
    1218 
    +We only use `trimQtvs` for /open/ families. For /closed/ families where we
    1219 
    +/unify/ (rather than match) the equation with the Wanted, it just doesn't work
    1220 
    +(#27994), because the substitution `S` has both meta-tyvars and instance-head
    1221 
    +tyvars in the range.  See (CF7).
    1166 1222
    1167 1223 
     Note [Exploiting closed type families] see `mkTopClosedFamEqFDs`
    1168 1224 
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    ... ... @@ -1194,9 +1250,6 @@ More precisely, here is the very clever Closed Family Fundep Algorithm (CFFA)
    1194 1250 
         with fresh unification vars in lhs and rhs for the quantified variables of the
    1195 1251 
         equation.
    1196 1252
    1197 
    -    Actually we take advantage of the substitution generated by the relevance
    1198 
    -    check, see (CF7) below.
    1199 
    -
    1200 1253 
     See Note [Relevance] for what "relevant" means.
    1201 1254 
     We need to take care about non-termination; see (CF3).
    1202 1255
    ... ... @@ -1303,7 +1356,7 @@ Key point: equations that are not relevant do not need to be considered for fund
    1303 1356 
       I was looking at non-termination for closed type families, but it's a small
    1304 1357 
       improvement in general.
    1305 1358
    1306 
    -  This bale-out is implementedn in `tryFDEqns`.
    1359 
    +  This bale-out is implemented in `tryFDEqns`.
    1307 1360
    1308 1361 
     (CF5) Consider (see "Yikes5" in #23162):
    1309 1362 
           type family F a where
    ... ... @@ -1353,32 +1406,20 @@ Key point: equations that are not relevant do not need to be considered for fund
    1353 1406 
              `app` Proxy @'[ty_n]
    1354 1407
    1355 1408 
       Every `app` call gives rise to a Wanted of the form:
    1356 
    -
    1357 1409 
         [W] MapId acc_i ++ MapId '[ty_i] ~ MapId (acc_i ++ '[ty_i])
    1358 
    -
    1359 1410 
       while the overall result type gives us a Wanted of the form
    1360 
    -
    1361 1411 
         [W] acc_n ++ '[ty_n] ~ [ty_1, ..., ty_n]
    1362 
    -
    1363 1412 
       By using (CFFA) on this result Wanted, we deduce that we must have
    1364 
    -
    1365 1413 
         acc_n ~ [ty_1, ..., ty_{n-1}]
    1366 
    -
    1367 1414 
       which is a flat list. Repeating the process, (CFFA) allows us to deduce that
    1368 
    -
    1369 1415 
         acc_i ~ [ty_1, ..., ty_{i-1}]
    1370 
    -
    1371 1416 
       for all i. This allows the other Wanteds to be solved directly, giving rise to
    1372 1417 
       proof terms with the typical triangular O(n^2) shape
    1373 
    -
    1374 1418 
         co_i = (O(i) proof that MapId acc_i ++ MapId '[ty_i] ~ acc_{i+1})
    1375 1419 
              ; (O(i) proof that acc_{i+1} ~ MapId (acc_i ++ '[ty_i]))
    1376 
    -
    1377 1420 
       However, /without/ (CFFA), 'acc_i' is not unified with a flat list but is left
    1378 1421 
       as the nested application:
    1379 
    -
    1380 1422 
         acc_i ~ (... (('[ty_1] ++ '[ty_2]) ++ '[ty_3]) ... ++ '[ty_{i-1}])
    1381 
    -
    1382 1423 
       This means that 'MapId acc_i' is stuck until we reduce the above, which takes
    1383 1424 
       O(i^2) type family reduction steps, instead of O(i). The same applies to
    1384 1425 
       the other proof term involving 'MapId (acc_i ++ '[ty_i])'.
    ... ... @@ -1388,29 +1429,77 @@ Key point: equations that are not relevant do not need to be considered for fund
    1388 1429 
       instead of relying on recursively built sub-proof terms, which brings down
    1389 1430 
       coercion sizes (in certain situations) from O(n^3) to O(n^2).
    1390 1431
    1391 
    -(CF7) Relevance.  When computing relevance in the Closed Family Fundep Algorithm,
    1392 
    -  for [W] F wlhs1 wlhs2 ~ wrhs, against an equation   F lhs1 lhs2 ~ rhs
    1393 
    -  we get back a pre-unifying substitution S that makes the two as equal as poss.
    1394 
    -  Then we use `trim_qtvs` in exactly the same way as in
    1395 
    -       (OF1) of Note [Exploiting open type families], to generate qtvs' and S'
    1396 
    -  Then we generate
    1397 
    -      FDEqns { fd_qtvs = qtvs', fd_eqs [ S'(lhs1) ~ wlhs1
    1398 
    -                                       , S'(lhs2) ~ wlhs2
    1399 
    -                                       , S'(rhs)  ~ wrhs ] }
    1400 
    -  Notice that we do /not/ apply S' to wlhs/wrhs.  These type contain unification
    1401 
    -  variables that we must actually unify! Example
    1432 
    +(CF7) Relevance.  The function `getRelevantBranches` finds the relevant branch(es)
    1433 
    +   using the (CFFA).   Given an equation
    1434 
    +       type family F a b where { ...; F lhs1 lhs2 = rhs; ... }
    1435 
    +   is the equation relevant for this Wanted?
    1436 
    +       [W] F wlhs1 wlhs2 ~ wrhs
    1437 
    +  We pre-unify [wrhs,wlhs1,wlhs2] against [rhs,lhs1,lhs2], getting back a
    1438 
    +  substitution `S` that makes the two as equal as poss. This substitution can bind
    1439 
    +  both /quantified/ type variables from the instance, and /unification variables/
    1440 
    +  from the solver. Moreover, both kind of type variable can appear in the range
    1441 
    +  of the substitution.
    1442 
    +
    1443 
    +  That's pretty complicated, so we are very cautious about using the returned
    1444 
    +  substitution `S`.  I had a long struggle (#27994) when we were previously trying to
    1445 
    +  apply that returned substitution as an optimisation.  But because type variables
    1446 
    +  can occur in kinds, it was a losing battle -- I ended up with TyVars from the
    1447 
    +  instance head escaping into the solver.   Consider
    1448 
    +      type F :: forall k. k -> *
    1449 
    +      type instance F k a where
    1450 
    +         F (k->*) (b::k->*) = Int
    1451 
    +      [W] F kappa (alpha::kappa) ~ Int
    1452 
    +  We unify the Wanted with the equation to get the substitution
    1453 
    +      [ kappa :-> k->*,  b :-> (alpha::k->*) ]
    1454 
    +  I tried using `trimQtvs` (see Note [trimQtvs]) but my head hurt
    1455 
    +  FAR too much: #27994 is an excellent example.
    1456 
    +
    1457 
    +  So here's the plan:
    1458 
    +  (A) As a fast-path optimisation, if `S` binds all the quantified variables of
    1459 
    +      the type-family equation (which is common), it's all easy: generate
    1460 
    +         FDEqns { fd_qtvs = []
    1461 
    +                , fd_eqs = [ S(lhs1) ~ wlhs1, S(lhs2) ~ wlhs2, S(rhs) ~ wrhs }
    1462 
    +      Note that we do not apply S to `wlhs1/2` or `wrhs`; see (CF9).
    1463 
    +      And note that `fd_qtvs` is empty, because `S` eliminates all the quantified
    1464 
    +      type variables.
    1465 
    +
    1466 
    +  (B) If not, then /discard `S` entirely/ and instead generate
    1467 
    +        FDEqns { fd_qtvs = qtvs
    1468 
    +               , fd_eqs = [ lhs ~ wlhs1, lhs2 ~ wlhs2, rhs ~ wrhs }
    1469 
    +      Now `instantiateFDEqns` will generate fresh unification variables for the
    1470 
    +      `qtvs` and the solver will in effect reconstruct `S`.
    1471 
    +
    1472 
    +(CF8) When computing relevance (Note [Relevance] (R2)) we use `noEarlierMatch`
    1473 
    +  on S(lhs).  But we must use /deep/ substitution on LHS. Consider
    1474 
    +     type family F (a :: k) r where
    1475 
    +       F @Type (Maybe Bool)              r = r      -- B0
    1476 
    +       F @Type ((f :: Type -> Type) Int) r = Bool   -- B1
    1477 
    +       F @k    ((g :: Type -> k) Int)    r = r      -- B2
    1478 
    +
    1479 
    +     [W] F @Type alpha Char ~ Char
    1480 
    +  The `tcUnifyTysForInjectivity` will return substitution
    1481 
    +      [k :-> Type, r :-> Char, alpha :-> (g :: Type->Type) Int], with g unbound
    1482 
    +  If we used `substTy` on the LHS-tys for B2 we'd get
    1483 
    +      lhs_tys' = [Type, (g :: Type -> k) Int, Char]
    1484 
    +  That's ill-kinded because of the free `k`; and (worse) when `noEarlierMatch` matches
    1485 
    +  lhs_tys' against earlier equations, (B1) will fail to match. So (B2) will be
    1486 
    +  judged relevant, even though it isn't.  Bad, bad. Use deep substitution.
    1487 
    +
    1488 
    +(CF9)  Notice that, in (CF7) when generating the fundep equations for the solver to
    1489 
    +  deal with, we do /not/ apply the pre-unifying substitution `S` to the Wanted types.
    1490 
    +  The types wlhs,wrhs contain meta-variables that we must actually unify! Example
    1402 1491 
          type family F a b where
    1403 1492 
            F [a] (Maybe b) = (a,  G b)
    1404 1493 
          [W] F alpha beta ~ (Int, [gamma])
    1405 1494 
       Pre-unification gives [alpha :-> [a], beta :-> Maybe b, a :-> Int]
    1406 
    -  This substitution eliminates the quantified variable `a` but not `b`, so we
    1407 
    -  want this:
    1408 
    -     FDEqns { fd_qtvs = [b], fd_eqs [ [Int] ~ alpha
    1409 
    -                                    , Maybe b ~ beta
    1410 
    -                                    , (Int,G b) ~ (Int, [gamma]) ] }
    1411 
    -
    1412 
    -  Notice also that by applying the substitution to the template but not to the
    1413 
    -  Wanted, we uphold the `fd_eqs` invariant in `FDEqns` (see its data type decl)
    1495 
    +  We don't want to substitute `alpha` away! In fact we just generate these eqns:
    1496 
    +     FDEqns { fd_qtvs = [a,b], fd_eqs [ [a] ~ alpha
    1497 
    +                                      , Maybe b ~ beta
    1498 
    +                                      , (a, G b) ~ (Int, [gamma]) ] }
    1499 
    +  with `fd_qtvs` being the quantified variables of the equation, the LHSs
    1500 
    +  being the types from the equation and the RHSs being the types from the Wanted.
    1501 
    +  Notice that we thereby uphold the `fd_eqs` invariant in `FDEqns` (see its data
    1502 
    +  type decl).
    1414 1503
    1415 1504 
     Note [Cache-caused loops]
    1416 1505 
     ~~~~~~~~~~~~~~~~~~~~~~~~~
    ... ... @@ -1517,8 +1606,8 @@ instantiateFunDepEqns (FDEqns { fd_qtvs = qtvs, fd_eqs = eqs })
    1517 1606 
         rev_eqs = reverse eqs
    1518 1607 
            -- (reverse eqs): See Note [Reverse order of fundep equations]
    1519 1608
    1520 
    -    -- The kinds of `qtvs` can have free variables, because of `trim_qtvs`
    1521 
    -    -- Example: T27828b
    1609 
    +    -- The kinds of `qtvs` can have free variables;
    1610 
    +    -- in the FDEqns produced by GHC.Tc.Instance.FunDeps.improveFromInstEnv
    1522 1611 
         empty_subst = mkEmptySubst $ mkInScopeSet $
    1523 1612 
                       tyCoVarsOfTypes (map tyVarKind qtvs)
    1524 1613

  • compiler/GHC/Tc/Utils/Unify.hs
    ... ... @@ -61,7 +61,6 @@ import GHC.Prelude
    61 61
    62 62 
     import GHC.Hs
    63 63 
     import GHC.Tc.Errors.Types ( HsCtxt(..) )
    64 
    -import GHC.Tc.Errors.Ppr   ( pprHsCtxt )
    65 64 
     import GHC.Tc.Utils.Concrete
    66 65 
     import GHC.Tc.Utils.Env
    67 66 
     import GHC.Tc.Utils.Instantiate
    ... ... @@ -2801,17 +2800,15 @@ uType_defer (UE { u_loc = loc, u_defer = ref
    2801 2800 
              -- snocBag: see Note [Work-list ordering] in GHC.Tc.Solver.Equality
    2802 2801
    2803 2802 
            -- Error trace only
    2804 
    -       -- NB. do *not* call tidyErrCtxt unless tracing is on,
    2805 
    -       --     because it is hugely expensive (#5631)
    2803 
    +       -- NB. do *not* call tidyErrCtxt because
    2804 
    +       -- (a) it is hugely expensive (#5631) and
    2805 
    +       -- (b) it crashes in some cases because because it reads
    2806 
    +       --     res_ty too early via FunResCtxt and getCheckExpType
    2806 2807 
            ; whenDOptM Opt_D_dump_tc_trace $
    2807 
    -         do { ctxt     <- getErrCtxt
    2808 
    -            ; err_ctxt <- tidyErrCtxt emptyTidyEnv ctxt
    2809 
    -            ; traceTc "utype_defer" $
    2810 
    -                vcat ( ppr role
    2811 
    -                     : debugPprType ty1
    2812 
    -                     : debugPprType ty2
    2813 
    -                     : map pprHsCtxt err_ctxt )
    2814 
    -            ; traceTc "utype_defer2" (ppr co) }
    2808 
    +         traceTc "utype_defer" $
    2809 
    +                vcat [ text "role:" <+> ppr role
    2810 
    +                     , text "ty1:" <+> debugPprType ty1
    2811 
    +                     , text "ty2:" <+> debugPprType ty2 ]
    2815 2812
    2816 2813 
            ; return co }
    2817 2814

  • compiler/GHC/Types/Var/Env.hs
    ... ... @@ -229,9 +229,17 @@ uniqAway' in_scope var
    229 229 
     -- | @unsafeGetFreshUnique in_scope@ finds a unique that is not in-scope in the
    230 230 
     -- given 'InScopeSet'. This must be used very carefully since one can very easily
    231 231 
     -- introduce non-unique 'Unique's this way. See Note [Local uniques].
    232 
    +--
    233 
    +-- Despite its name, there is nothing unsafe about it, provided you
    234 
    +-- know that all it does is find a unique not in the in-scope set.
    235 
    +-- Two calls with the same in-scope set will (of course) produce the
    236 
    +-- same unique.
    232 237 
     unsafeGetFreshLocalUnique :: InScopeSet -> Unique
    233 238 
     unsafeGetFreshLocalUnique (InScope set)
    234 239 
       | Just (uniq,_) <- Word64Map.lookupLT (getKey maxLocalUnique) (ufmToIntMap $ getUniqSet set)
    240 
    +       -- (lookupLT k m) finds the largest (key,value) in `m` such that key < k
    241 
    +       -- So if we make k=maxLocalUnique we'll just get the largest key in `m`
    242 
    +       -- Then all we need do is increment it, and that'll give us a fresh one
    235 243 
       , let uniq' = mkLocalUnique uniq
    236 244 
       , not $ uniq' `ltUnique` minLocalUnique
    237 245 
       = incrUnique uniq'

  • testsuite/tests/typecheck/should_compile/T27994.hs
    1 
    +{-# LANGUAGE AllowAmbiguousTypes #-}
    2 
    +{-# LANGUAGE DataKinds #-}
    3 
    +{-# LANGUAGE FunctionalDependencies #-}
    4 
    +{-# LANGUAGE GADTs #-}
    5 
    +{-# LANGUAGE TypeFamilies #-}
    6 
    +module  T27994a (l2) where
    7 
    +
    8 
    +import Data.Kind (Constraint, Type)
    9 
    +
    10 
    +l1 :: [String]
    11 
    +l1 = ["hello", "world!"]
    12 
    +
    13 
    +l2 :: [Int]
    14 
    +l2 = gmap (HCons length HNil) l1
    15 
    +
    16 
    +-----
    17 
    +
    18 
    +type HList :: [Type] -> Type
    19 
    +data HList p where
    20 
    +  HNil :: HList '[]
    21 
    +  HCons :: x -> HList xs -> HList (x:xs)
    22 
    +
    23 
    +type ($$) :: k -> [Type] -> Type
    24 
    +type family s $$ p where
    25 
    +  (s :: Type)      $$ '[]   = s
    26 
    +  (s :: Type -> k) $$ (a:b) = s a $$ b
    27 
    +
    28 
    +type Doms :: [Type] -> [Type]
    29 
    +type family Doms t where
    30 
    +  Doms '[]            = '[]
    31 
    +  Doms ((a -> b) : t) = a : Doms t
    32 
    +
    33 
    +type Codoms :: [Type] -> [Type]
    34 
    +type family Codoms t where
    35 
    +  Codoms '[]            = '[]
    36 
    +  Codoms ((a -> b) : t) = b : Codoms t
    37 
    +
    38 
    +type GMap :: k -> [Type] -> Constraint
    39 
    +class GMap (s :: k) t | t -> k where
    40 
    +  gmap :: HList t -> s $$ Doms t -> s $$ Codoms t
    41 
    +
    42 
    +instance GMap [] '[a -> b] where
    43 
    +  gmap :: HList '[a -> b] -> [a] -> [b]
    44 
    +  gmap (HCons f HNil) = go
    45 
    +    where
    46 
    +      go :: [a] -> [b]
    47 
    +      go []     = []
    48 
    +      go (x:xs) = f x : go xs

  • testsuite/tests/typecheck/should_compile/T27994a.hs
    1 
    +{-# LANGUAGE DataKinds, TypeFamilies, PolyKinds, GADTs, AllowAmbiguousTypes #-}
    2 
    +module T27994 where
    3 
    +
    4 
    +import Data.Kind (Type)
    5 
    +import Data.Proxy (Proxy)
    6 
    +
    7 
    +type F :: forall{k}. k -> Type -> Type
    8 
    +type family F s x where
    9 
    +   F (s :: Type -> k) (Proxy s) = Int
    10 
    +
    11 
    +f :: forall k (s :: k) x. F s x -> x
    12 
    +f _ = undefined
    13 
    +
    14 
    +g :: Proxy Maybe -> ()
    15 
    +g _ = ()
    16 
    +
    17 
    +data T a where
    18 
    +  MkT :: T Int
    19 
    +
    20 
    +test :: T a -> ()
    21 
    +test t = (\y -> case t of MkT -> g y) (f (3 :: Int))
    22 
    +
    23 
    +{- [W] F @k_azX (s_azY::k_azX) p_azN ~ Int
    24 
    +
    25 
    +unify   [*->k,      s::*->k,  Proxy @(*->k) (s::*->k), Int]
    26 
    +          ~ [k_azX, s_azY::k_azX, p_azN,                   Int]
    27 
    +
    28 
    +  -->   [ k_azX :-> (* -> k)
    29 
    +        , s     :-> s_azY::k_azX
    30 
    +        , p_azN :-> Proxy @(*->k) (s::*->k) ]
    31 
    +
    32 
    +  fixpt -->   [ k_azX :-> Type -> k
    33 
    +              , s     :-> s_azY::(Type -> k)
    34 
    +              , p_azN :-> Proxy @(Type->k) (s::k_azX) ]
    35 
    +
    36 
    +Generate a [W] for each pair
    37 
    +    [W] k ~ k_azX
    38 
    +    [W] s ~ s_azY
    39 
    +    [W] Proxy s ~ p_azN
    40 
    +    [W] Int ~ Int
    41 
    +As an opt (claim) apply subst first
    42 
    +    [W] k_azX ~ k_azX
    43 
    +    [W] s_azY ~ s_azY
    44 
    +    [W] Proxy s_azY ~ p_azN
    45 
    +    [W] Int ~ Int
    46 
    +
    47 
    +-- [W] F @k_azX s_azY[tau] p_azN ~ Int
    48 
    +-- Want: fresh k' s'
    49 
    +-- [W] k' ~ k_azX
    50 
    +-- [W] s':k' ~ s_azY:k_azX
    51 
    +-- [W] Proxy s' ~ x
    52 
    +-}
    53 
    +

  • testsuite/tests/typecheck/should_compile/T27994b.hs
    1 
    +{-# LANGUAGE TypeFamilies, TypeFamilyDependencies #-}
    2 
    +
    3 
    +
    4 
    +module T27994b where
    5 
    +import Data.Proxy
    6 
    +
    7 
    +type family G a where G Int = Char
    8 
    +type family F a b = r | r -> a
    9 
    +type instance F a   [c]  = (a, G a)      -- instance 1
    10 
    +type instance F Int Bool = (Int, Bool)   -- instance 2
    11 
    +
    12 
    +h :: Proxy a -> F a Bool
    13 
    +h = h
    14 
    +k :: (Int, b) -> b
    15 
    +k = k
    16 
    +
    17 
    +test = k (h Proxy) `seq` ()   -- [W] F alpha Bool ~ (Int, gamma)

  • testsuite/tests/typecheck/should_compile/all.T
    ... ... @@ -972,4 +972,6 @@ test('T27557', normal, compile, [''])
    972 972 
     test('T27664', normal, compile, [''])
    973 973 
     test('T27916', normal, compile, [''])
    974 974 
     test('T26543_orig', normal, compile, [''])
    975 
    -
    975 
    +test('T27994',  normal, compile, [''])
    976 
    +test('T27994a', normal, compile, [''])
    977 
    +test('T27994b', normal, compile, [''])

    • —
    View it on GitLab.
    You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications · Help Notification message regarding https://gitlab.haskell.org/ghc/ghc/-/compare/d842c67282c6719534e11cdf2c14863a3af245d8...3b60ae7e105f6450243451a8e8b06b4474d34fdb at 1793453069