Wibble to Taming the Kind Inference Monster
authorSimon Peyton Jones <simonpj@microsoft.com>
Fri, 7 Dec 2018 14:25:30 +0000 (14:25 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 7 Dec 2018 14:44:26 +0000 (14:44 +0000)
I had allowed rename/should_fail/T15828 (Trac #15828) to regress a bit.
The main payload of this patch is to fix that problem, at the cost of
more contortions in checkConsistentFamInst.  Oh well, at least they are
highly localised.

I also update the -ddump-types code in TcRnDriver to print out some
more expicit information about each type constructor, thus instead of

   DF{3} :: forall k. * -> k -> *

we get

   data family DF{3} :: forall k. * -> k -> *

Remember, this is debug-printing only.  This change is the reason
that so many .stderr files change.

38 files changed:
compiler/typecheck/ClsInst.hs
compiler/typecheck/TcInstDcls.hs
compiler/typecheck/TcRnDriver.hs
compiler/typecheck/TcValidity.hs
compiler/types/Coercion.hs
compiler/types/FamInstEnv.hs
testsuite/tests/dependent/should_compile/T15743.stderr
testsuite/tests/dependent/should_compile/T15743e.stderr
testsuite/tests/indexed-types/should_compile/T15711.stderr
testsuite/tests/indexed-types/should_compile/T15852.stderr
testsuite/tests/indexed-types/should_compile/T3017.stderr
testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr
testsuite/tests/indexed-types/should_fail/SimpleFail2a.stderr
testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr
testsuite/tests/indexed-types/should_fail/T11450.stderr
testsuite/tests/indexed-types/should_fail/T12041.stderr
testsuite/tests/indexed-types/should_fail/T14230.stderr
testsuite/tests/indexed-types/should_fail/T9160.stderr
testsuite/tests/partial-sigs/should_compile/ADT.stderr
testsuite/tests/partial-sigs/should_compile/DataFamilyInstanceLHS.stderr
testsuite/tests/partial-sigs/should_compile/Meltdown.stderr
testsuite/tests/partial-sigs/should_compile/NamedWildcardInDataFamilyInstanceLHS.stderr
testsuite/tests/partial-sigs/should_compile/NamedWildcardInTypeFamilyInstanceLHS.stderr
testsuite/tests/partial-sigs/should_compile/SkipMany.stderr
testsuite/tests/partial-sigs/should_compile/TypeFamilyInstanceLHS.stderr
testsuite/tests/polykinds/T14450.stderr
testsuite/tests/polykinds/T15592.stderr
testsuite/tests/polykinds/T15592b.stderr
testsuite/tests/rename/should_fail/T15828.stderr
testsuite/tests/roles/should_compile/Roles1.stderr
testsuite/tests/roles/should_compile/Roles14.stderr
testsuite/tests/roles/should_compile/Roles2.stderr
testsuite/tests/roles/should_compile/Roles3.stderr
testsuite/tests/roles/should_compile/Roles4.stderr
testsuite/tests/roles/should_compile/T8958.stderr
testsuite/tests/th/TH_Roles2.stderr
testsuite/tests/typecheck/should_compile/T12763.stderr
testsuite/tests/typecheck/should_compile/tc231.stderr

index 1b6ab12..516b898 100644 (file)
@@ -55,6 +55,8 @@ data AssocInstInfo
   = NotAssociated
   | InClsInst { ai_class    :: Class
               , ai_tyvars   :: [TyVar]      -- ^ The /scoped/ tyvars of the instance
+                                            -- Why scoped?  See bind_me in
+                                            -- TcValidity.checkConsistentFamInst
               , ai_inst_env :: VarEnv Type  -- ^ Maps /class/ tyvars to their instance types
                 -- See Note [Matching in the consistent-instantation check]
     }
index 8d2ef94..e2150e7 100644 (file)
@@ -484,7 +484,7 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = hs_ty, cid_binds = binds
                            fst $ splitForAllVarBndrs dfun_ty
               visible_skol_tvs = drop n_inferred skol_tvs
 
-        ; traceTc "tcLocalInstDecl 1" (ppr dfun_ty $$ ppr (invisibleTyBndrCount dfun_ty) $$ ppr skol_tvs $$ ppr visible_skol_tvs)
+        ; traceTc "tcLocalInstDecl 1" (ppr dfun_ty $$ ppr (invisibleTyBndrCount dfun_ty) $$ ppr skol_tvs)
 
         -- Next, process any associated types.
         ; (datafam_stuff, tyfam_insts)
index b13ae21..3b12837 100644 (file)
@@ -2745,11 +2745,12 @@ ppr_tycons debug fam_insts type_env
                      | otherwise  = isExternalName (tyConName tycon) &&
                                     not (tycon `elem` fi_tycons)
     ppr_tc tc
-       = vcat [ ppWhen show_roles $
-                hang (text "type role" <+> ppr tc)
-                   2 (hsep (map ppr roles))
-              , hang (ppr tc <> braces (ppr (tyConArity tc)) <+> dcolon)
-                   2 (ppr (tidyTopType (tyConKind tc))) ]
+       = vcat [ hang (ppr (tyConFlavour tc) <+> ppr tc
+                      <> braces (ppr (tyConArity tc)) <+> dcolon)
+                   2 (ppr (tidyTopType (tyConKind tc)))
+              , nest 2 $
+                ppWhen show_roles $
+                text "roles" <+> (sep (map ppr roles)) ]
        where
          show_roles = debug || not (all (== boring_role) roles)
          roles = tyConRoles tc
@@ -2758,6 +2759,9 @@ ppr_tycons debug fam_insts type_env
             -- Matches the choice in IfaceSyn, calls to pprRoles
 
     ppr_ax ax = ppr (coAxiomToIfaceDecl ax)
+      -- We go via IfaceDecl rather than using pprCoAxiom
+      -- This way we get the full axiom (both LHS and RHS) with
+      -- wildcard binders tidied to _1, _2, etc.
 
 ppr_datacons :: Bool -> TypeEnv -> SDoc
 ppr_datacons debug type_env
index f82e394..ca5db45 100644 (file)
@@ -39,8 +39,8 @@ import Class
 import TyCon
 
 -- others:
-import IfaceType( pprIfaceType )
-import ToIface( toIfaceType )
+import IfaceType( pprIfaceType, pprIfaceTypeApp )
+import ToIface( toIfaceType, toIfaceTyCon, toIfaceTcArgs )
 import HsSyn            -- HsType
 import TcRnMonad        -- TcType, amongst others
 import TcEnv       ( tcInitTidyEnv, tcInitOpenTidyEnv )
@@ -1931,7 +1931,10 @@ checkConsistentFamInst (InClsInst { ai_class = clas
                        fam_tc branch
   = do { traceTc "checkConsistentFamInst" (vcat [ ppr inst_tvs
                                                 , ppr arg_triples
-                                                , ppr mini_env ])
+                                                , ppr mini_env
+                                                , ppr ax_tvs
+                                                , ppr ax_arg_tys
+                                                , ppr arg_triples ])
        -- Check that the associated type indeed comes from this class
        -- See [Mismatched class methods and associated type families]
        -- in TcInstDecls.
@@ -1941,15 +1944,14 @@ checkConsistentFamInst (InClsInst { ai_class = clas
        ; check_match arg_triples
        }
   where
-    CoAxBranch { cab_eta_tvs = eta_tvs, cab_lhs = pats } = branch
-    at_arg_tys = pats ++ mkTyVarTys eta_tvs
+    (ax_tvs, ax_arg_tys, _) = etaExpandCoAxBranch branch
 
     arg_triples :: [(Type,Type, ArgFlag)]
     arg_triples = [ (cls_arg_ty, at_arg_ty, vis)
                   | (fam_tc_tv, vis, at_arg_ty)
                        <- zip3 (tyConTyVars fam_tc)
-                               (tyConArgFlags fam_tc at_arg_tys)
-                               at_arg_tys
+                               (tyConArgFlags fam_tc ax_arg_tys)
+                               ax_arg_tys
                   , Just cls_arg_ty <- [lookupVarEnv mini_env fam_tc_tv] ]
 
     pp_wrong_at_arg vis
@@ -1960,19 +1962,23 @@ checkConsistentFamInst (InClsInst { ai_class = clas
 
     -- Fiddling around to arrange that wildcards unconditionally print as "_"
     -- We only need to print the LHS, not the RHS at all
-    expected_args = [ lookupVarEnv mini_env at_tv `orElse` mk_wildcard at_tv
-                    | at_tv <- tyConTyVars fam_tc ]
+    -- See Note [Printing conflicts with class header]
+    (tidy_env1, _) = tidyVarBndrs emptyTidyEnv inst_tvs
+    (tidy_env2, _) = tidyCoAxBndrsForUser tidy_env1 (ax_tvs \\ inst_tvs)
+
+    pp_expected_ty = pprIfaceTypeApp topPrec (toIfaceTyCon fam_tc) $
+                     toIfaceTcArgs fam_tc $
+                     [ case lookupVarEnv mini_env at_tv of
+                         Just cls_arg_ty -> tidyType tidy_env2 cls_arg_ty
+                         Nothing         -> mk_wildcard at_tv
+                     | at_tv <- tyConTyVars fam_tc ]
+
+    pp_actual_ty = pprIfaceTypeApp topPrec (toIfaceTyCon fam_tc) $
+                   toIfaceTcArgs fam_tc $
+                   tidyTypes tidy_env2 ax_arg_tys
+
     mk_wildcard at_tv = mkTyVarTy (mkTyVar tv_name (tyVarKind at_tv))
     tv_name = mkInternalName (mkAlphaTyVarUnique 1) (mkTyVarOcc "_") noSrcSpan
-    pp_expected_ty = pprIfaceType (toIfaceType (mkTyConApp fam_tc expected_args))
-                     -- Do /not/ tidy, because that will rename all those "_"
-                     -- variables we have put in.  And (I think) the intance type
-                     --  is already tidy
-
---    actual_ty   = mkTyConApp fam_tc at_arg_tys
---    (tidy_env, bndrs) = tidyCoAxBndrs (tyCoVarsOfTypesList [expected_ty, actual_ty])
---    pp_actual_ty pprPrecTypeX tidy_env topPrec actual_ty
-    pp_actual_ty = pprCoAxBranchLHS fam_tc branch
 
     -- For check_match, bind_me, see
     -- Note [Matching in the consistent-instantation check]
@@ -1987,8 +1993,8 @@ checkConsistentFamInst (InClsInst { ai_class = clas
       | otherwise
       = addErrTc (pp_wrong_at_arg vis)
 
-    -- The scoped type variables from the class-instance header
-    -- should not be alpha-raenamed.
+    -- The /scoped/ type variables from the class-instance header
+    -- should not be alpha-renamed.  Inferred ones can be.
     no_bind_set = mkVarSet inst_tvs
     bind_me tv | tv `elemVarSet` no_bind_set = Skolem
                | otherwise                   = BindMe
@@ -2123,6 +2129,46 @@ Here the instance is kind-indexed and really looks like
 But if the 'b' didn't scope, we would make F's instance too
 poly-kinded.
 
+Note [Printing conflicts with class header]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It's remarkably painful to give a decent error message for conflicts
+with the class header.  Consider
+   clase C b where
+     type F a b c
+   instance C [b] where
+     type F x Int _ _ = ...
+
+Here we want to report a conflict between
+    Expected: F _ [b] _
+    Actual:   F x Int _ _
+
+But if the type instance shadows the class variable like this
+(rename/should_fail/T15828):
+   instance C [b] where
+     type forall b. F x (Tree b) _ _ = ...
+
+then we must use a fresh variable name
+    Expected: F _ [b] _
+    Actual:   F x [b1] _ _
+
+Notice that:
+  - We want to print an underscore in the "Expected" type in
+    positions where the class header has no influence over the
+    parameter.  Hence the fancy footwork in pp_expected_ty
+
+  - Although the binders in the axiom are aready tidy, we must
+    re-tidy them to get a fresh variable name when we shadow
+
+  - The (ax_tvs \\ inst_tvs) is to avoid tidying one of the
+    class-instance variables a second time, from 'a' to 'a1' say.
+    Remember, the ax_tvs of the axiom share identity with the
+    class-instance variables, inst_tvs..
+
+  - We use tidyCoAxBndrsForUser to get underscores rather than
+    _1, _2, etc in the axiom tyvars; see the definition of
+    tidyCoAxBndrsForUser
+
+This all seems absurdly complicated.
 
 Note [Unused explicitly bound variables in a family pattern]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
index a55deeb..ff0c9c5 100644 (file)
@@ -98,7 +98,8 @@ module Coercion (
 
         -- * Pretty-printing
         pprCo, pprParendCo,
-        pprCoAxiom, pprCoAxBranch, pprCoAxBranchLHS, pprCoAxBranchUser,
+        pprCoAxiom, pprCoAxBranch, pprCoAxBranchLHS,
+        pprCoAxBranchUser, tidyCoAxBndrsForUser,
         etaExpandCoAxBranch,
 
         -- * Tidying
@@ -189,7 +190,7 @@ pprCoAxiom :: CoAxiom br -> SDoc
 -- Used in debug-printing only
 pprCoAxiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
   = hang (text "axiom" <+> ppr ax <+> dcolon)
-       2 (vcat (map (pprCoAxBranch tc) (fromBranches branches)))
+       2 (vcat (map (pprCoAxBranchUser tc) (fromBranches branches)))
 
 pprCoAxBranchUser :: TyCon -> CoAxBranch -> SDoc
 -- Used when printing injectivity errors (FamInst.makeInjectivityErrors)
@@ -237,9 +238,9 @@ ppr_co_ax_branch ppr_rhs fam_tc branch
     pp_lhs = pprIfaceTypeApp topPrec (toIfaceTyCon fam_tc)
                              (tidyToIfaceTcArgs tidy_env fam_tc ee_lhs)
 
-    (tidy_env, bndrs') = tidyCoAxBndrs ee_tvs
+    (tidy_env, bndrs') = tidyCoAxBndrsForUser emptyTidyEnv ee_tvs
 
-tidyCoAxBndrs :: [Var] -> (TidyEnv, [Var])
+tidyCoAxBndrsForUser :: TidyEnv -> [Var] -> (TidyEnv, [Var])
 -- Tidy wildcards "_1", "_2" to "_", and do not return them
 -- in the list of binders to be printed
 -- This is so that in error messages we see
@@ -248,11 +249,10 @@ tidyCoAxBndrs :: [Var] -> (TidyEnv, [Var])
 --     forall a _1 _2. F _1 [a] _2 = ...
 --
 -- This is a rather disgusting function
-tidyCoAxBndrs tcvs
+tidyCoAxBndrsForUser init_env tcvs
   = (tidy_env, reverse tidy_bndrs)
   where
-    (tidy_env, tidy_bndrs) = foldl tidy_one (empty_env, []) tcvs
-    empty_env = mkEmptyTidyEnv (initTidyOccEnv [mkTyVarOcc "_"])
+    (tidy_env, tidy_bndrs) = foldl tidy_one (init_env, []) tcvs
 
     tidy_one (env@(occ_env, subst), rev_bndrs') bndr
       | is_wildcard bndr = (env_wild, rev_bndrs')
index 149ff3f..c6dcab6 100644 (file)
@@ -224,7 +224,7 @@ pprFamInst :: FamInst -> SDoc
 pprFamInst (FamInst { fi_flavor = flavor, fi_axiom = ax
                     , fi_tvs = tvs, fi_tys = tys, fi_rhs = rhs })
   = hang (ppr_tc_sort <+> text "instance"
-             <+> pprCoAxBranch (coAxiomTyCon ax) (coAxiomSingleBranch ax))
+             <+> pprCoAxBranchUser (coAxiomTyCon ax) (coAxiomSingleBranch ax))
        2 (whenPprDebug debug_stuff)
   where
     ppr_tc_sort = case flavor of
index f44c430..ea84b95 100644 (file)
@@ -1,6 +1,7 @@
 TYPE CONSTRUCTORS
-  type role T nominal nominal nominal phantom phantom phantom
-  T{6} :: forall {k1} k2 (k3 :: k2). Proxy k3 -> k1 -> k2 -> *
+  data type T{6} ::
+    forall {k1} k2 (k3 :: k2). Proxy k3 -> k1 -> k2 -> *
+    roles nominal nominal nominal phantom phantom phantom
 Dependent modules: []
 Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
                      integer-gmp-1.0.2.0]
index f96da68..dcfdd2e 100644 (file)
@@ -1,16 +1,26 @@
 TYPE CONSTRUCTORS
-  type role T
-    nominal nominal nominal nominal nominal nominal phantom phantom representational nominal nominal phantom nominal phantom
-  T{14} ::
+  data type T{14} ::
     forall {k1} {k2} {k3} (k4 :: k2) k5. forall k6 ->
     k6
     -> Proxy k4
     -> (k3 -> *)
     -> k3
     -> forall (k7 :: k1). Proxy k7 -> forall (k8 :: k5). Proxy k8 -> *
-  type role T2
-    nominal nominal nominal nominal nominal phantom phantom representational nominal nominal phantom nominal nominal phantom
-  T2{14} ::
+    roles nominal
+          nominal
+          nominal
+          nominal
+          nominal
+          nominal
+          phantom
+          phantom
+          representational
+          nominal
+          nominal
+          phantom
+          nominal
+          phantom
+  data type T2{14} ::
     forall {k1} {k2} (k3 :: k2) k7. forall k4 ->
     k4
     -> Proxy k3
@@ -18,6 +28,20 @@ TYPE CONSTRUCTORS
     -> k7
     -> forall (k5 :: k1).
        Proxy k5 -> forall k6 (k8 :: k6). Proxy k8 -> *
+    roles nominal
+          nominal
+          nominal
+          nominal
+          nominal
+          phantom
+          phantom
+          representational
+          nominal
+          nominal
+          phantom
+          nominal
+          nominal
+          phantom
 DATA CONSTRUCTORS
   MkT2 :: forall {k7} {k1} {k2 :: k1} {k3} {k4 :: k3} {k5} {k6 :: k5}
                  (f :: k7 -> *) (c :: k7) k8 (a :: k8) (b :: Proxy k2)
index 2a01248..7101dce 100644 (file)
@@ -1,7 +1,7 @@
 TYPE CONSTRUCTORS
-  C{1} :: * -> Constraint
-  type role F nominal nominal
-  F{2} :: forall a. Maybe a -> *
+  class C{1} :: * -> Constraint
+  associated type family F{2} :: forall a. Maybe a -> *
+    roles nominal nominal
 Dependent modules: []
 Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
                      integer-gmp-1.0.2.0]
index 6908d00..9024739 100644 (file)
@@ -1,14 +1,13 @@
 TYPE CONSTRUCTORS
-  type role DF nominal nominal nominal
-  DF{3} :: forall k. * -> k -> *
+  data family DF{3} :: forall k. * -> k -> *
+    roles nominal nominal nominal
 COERCION AXIOMS
   axiom T15852.D:R:DFProxyProxy0 ::
     forall k1 k2 (j :: k1) (c :: k2).
       DF (Proxy c) = T15852.R:DFProxyProxy k1 k2 j c
 FAMILY INSTANCES
   data instance forall k1 k2 (j :: k1) (c :: k2).
-                  DF (Proxy c) = T15852.R:DFProxyProxy k1 k2 j c
-                    -- Defined at T15852.hs:10:15
+                  DF (Proxy c) -- Defined at T15852.hs:10:15
 Dependent modules: []
 Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
                      integer-gmp-1.0.2.0]
index 9cf3196..8b5f868 100644 (file)
@@ -5,10 +5,10 @@ TYPE SIGNATURES
   test2 ::
     forall c a b. (Coll c, Num a, Num b, Elem c ~ (a, b)) => c -> c
 TYPE CONSTRUCTORS
-  Coll{1} :: * -> Constraint
-  type role Elem nominal
-  Elem{1} :: * -> *
-  ListColl{1} :: * -> *
+  class Coll{1} :: * -> Constraint
+  associated type family Elem{1} :: * -> *
+    roles nominal
+  data type ListColl{1} :: * -> *
 COERCION AXIOMS
   axiom Foo.D:R:ElemListColl :: Elem (ListColl a) = a
 DATA CONSTRUCTORS
index 8e268d6..e7065cf 100644 (file)
@@ -47,7 +47,7 @@ ExplicitForAllFams4b.hs:16:25: error:
 ExplicitForAllFams4b.hs:23:3: error:
     • Type indexes must match class instance head
       Expected: CT Int _
-        Actual: CT [a] (a, a) -- Defined at ExplicitForAllFams4b.hs:23:20
+        Actual: CT [a] (a, a)
     • In the type instance declaration for ‘CT’
       In the instance declaration for ‘C Int’
 
@@ -65,7 +65,7 @@ ExplicitForAllFams4b.hs:23:20: error:
 ExplicitForAllFams4b.hs:24:3: error:
     • Type indexes must match class instance head
       Expected: CT Int _
-        Actual: CT _ _ -- Defined at ExplicitForAllFams4b.hs:24:20
+        Actual: CT _ _
     • In the type instance declaration for ‘CT’
       In the instance declaration for ‘C Int’
 
@@ -78,7 +78,7 @@ ExplicitForAllFams4b.hs:24:15: error:
 ExplicitForAllFams4b.hs:26:3: error:
     • Type indexes must match class instance head
       Expected: CD Int _
-        Actual: CD [a] (a, a) -- Defined at ExplicitForAllFams4b.hs:26:20
+        Actual: CD [a] (a, a)
     • In the data instance declaration for ‘CD’
       In the instance declaration for ‘C Int’
 
@@ -96,7 +96,7 @@ ExplicitForAllFams4b.hs:26:20: error:
 ExplicitForAllFams4b.hs:27:3: error:
     • Type indexes must match class instance head
       Expected: CD Int _
-        Actual: CD _ _ -- Defined at ExplicitForAllFams4b.hs:27:20
+        Actual: CD _ _
     • In the data instance declaration for ‘CD’
       In the instance declaration for ‘C Int’
 
index b21375c..ebe0e53 100644 (file)
@@ -2,7 +2,7 @@
 SimpleFail2a.hs:11:3: error:
     • Type indexes must match class instance head
       Expected: Sd Int
-        Actual: Sd a -- Defined at SimpleFail2a.hs:11:11
+        Actual: Sd a
     • In the data instance declaration for ‘Sd’
       In the instance declaration for ‘C Int’
 
index b3dd8ef..114f7e1 100644 (file)
@@ -2,6 +2,6 @@
 SimpleFail9.hs:16:3: error:
     • Type indexes must match class instance head
       Expected: S7 (a, Int)
-        Actual: S7 (b, Int) -- Defined at SimpleFail9.hs:16:8
+        Actual: S7 (b, Int)
     • In the data instance declaration for ‘S7’
       In the instance declaration for ‘C7 Char (a, Int)’
index f5be9d4..0ecdfb9 100644 (file)
@@ -2,6 +2,6 @@
 T11450.hs:9:3: error:
     • Type indexes must match class instance head
       Expected: T (Either a b)
-        Actual: T (Either b a) -- Defined at T11450.hs:9:8
+        Actual: T (Either b a)
     • In the type instance declaration for ‘T’
       In the instance declaration for ‘C (Either a b)’
index d16a9cc..4c00866 100644 (file)
@@ -2,6 +2,6 @@
 T12041.hs:12:3: error:
     • Type indexes must match class instance head
       Expected: Ob @i (I @{i} @{i})
-        Actual: Ob @* (I @{*} @{*}) -- Defined at T12041.hs:12:8
+        Actual: Ob @* (I @{*} @{*})
     • In the type instance declaration for ‘Ob’
       In the instance declaration for ‘Category I’
index 174a15a..55de0b7 100644 (file)
@@ -2,6 +2,6 @@
 T14230.hs:11:3: error:
     • Type indexes must match class instance head
       Expected: CD @(Maybe a)
-        Actual: CD @(k -> *) -- Defined at T14230.hs:11:8
+        Actual: CD @(k -> *)
     • In the data instance declaration for ‘CD’
       In the instance declaration for ‘C (Maybe a)’
index 36a1cb6..e918013 100644 (file)
@@ -2,6 +2,6 @@
 T9160.hs:19:3: error:
     • Type indexes must match class instance head
       Expected: F @*
-        Actual: F @(* -> *) -- Defined at T9160.hs:19:8
+        Actual: F @(* -> *)
     • In the type instance declaration for ‘F’
       In the instance declaration for ‘C (a :: *)’
index 385a44b..421a03f 100644 (file)
@@ -1,7 +1,7 @@
 TYPE SIGNATURES
   bar :: Int -> Foo Bool () Int
 TYPE CONSTRUCTORS
-  Foo{3} :: * -> * -> * -> *
+  data type Foo{3} :: * -> * -> * -> *
 DATA CONSTRUCTORS
   Foo :: forall x y z. x -> y -> z -> Foo x y z
 Dependent modules: []
index 6f68f3c..f17860f 100644 (file)
@@ -1,9 +1,9 @@
 TYPE SIGNATURES
   foo :: Sing 'A
 TYPE CONSTRUCTORS
-  MyKind{0} :: *
-  type role Sing nominal nominal
-  Sing{2} :: forall k. k -> *
+  data type MyKind{0} :: *
+  data family Sing{2} :: forall k. k -> *
+    roles nominal nominal
 COERCION AXIOMS
   axiom DataFamilyInstanceLHS.D:R:SingMyKind_0 ::
       Sing = DataFamilyInstanceLHS.R:SingMyKind_
@@ -13,8 +13,7 @@ DATA CONSTRUCTORS
   SingA :: Sing 'A
   SingB :: Sing 'B
 FAMILY INSTANCES
-  data instance Sing _ = DataFamilyInstanceLHS.R:SingMyKind_ _
-                  -- Defined at DataFamilyInstanceLHS.hs:8:15
+  data instance Sing _ -- Defined at DataFamilyInstanceLHS.hs:8:15
 Dependent modules: []
 Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
                      integer-gmp-1.0.2.0]
index a40ecfe..8e14ffd 100644 (file)
@@ -4,8 +4,8 @@ TYPE SIGNATURES
     forall param1 param2.
     NukeMonad param1 param2 () -> NukeMonad param1 param2 ()
 TYPE CONSTRUCTORS
-  type role NukeMonad phantom phantom phantom
-  NukeMonad{3} :: * -> * -> * -> *
+  data type NukeMonad{3} :: * -> * -> * -> *
+    roles phantom phantom phantom
 CLASS INSTANCES
   instance Functor (NukeMonad a b) -- Defined at Meltdown.hs:8:10
   instance Applicative (NukeMonad a b)
index 94245d6..0569228 100644 (file)
@@ -1,7 +1,7 @@
 TYPE CONSTRUCTORS
-  MyKind{0} :: *
-  type role Sing nominal nominal
-  Sing{2} :: forall k. k -> *
+  data type MyKind{0} :: *
+  data family Sing{2} :: forall k. k -> *
+    roles nominal nominal
 COERCION AXIOMS
   axiom NamedWildcardInDataFamilyInstanceLHS.D:R:SingMyKind_a0 ::
       Sing = NamedWildcardInDataFamilyInstanceLHS.R:SingMyKind_a
@@ -11,8 +11,7 @@ DATA CONSTRUCTORS
   SingA :: Sing 'A
   SingB :: Sing 'B
 FAMILY INSTANCES
-  data instance Sing
-                  _a = NamedWildcardInDataFamilyInstanceLHS.R:SingMyKind_a _a
+  data instance Sing _a
                   -- Defined at NamedWildcardInDataFamilyInstanceLHS.hs:8:15
 Dependent modules: []
 Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
index 5a709ff..690a1c6 100644 (file)
@@ -1,6 +1,6 @@
 TYPE CONSTRUCTORS
-  type role F nominal
-  F{1} :: * -> *
+  type family F{1} :: * -> *
+    roles nominal
 COERCION AXIOMS
   axiom NamedWildcardInTypeFamilyInstanceLHS.D:R:F :: F _t = Int
 Dependent modules: []
index 0ee0a34..25555b4 100644 (file)
@@ -4,7 +4,7 @@ TYPE SIGNATURES
   skipMany' ::
     forall tok st a. GenParser tok st a -> GenParser tok st ()
 TYPE CONSTRUCTORS
-  GenParser{3} :: * -> * -> * -> *
+  data type GenParser{3} :: * -> * -> * -> *
 DATA CONSTRUCTORS
   GenParser :: forall tok st a. tok -> st -> a -> GenParser tok st a
 Dependent modules: []
index 8f24ba1..e0a2bfc 100644 (file)
@@ -1,8 +1,8 @@
 TYPE SIGNATURES
   foo :: F Int Char -> Int
 TYPE CONSTRUCTORS
-  type role F nominal nominal
-  F{2} :: * -> * -> *
+  type family F{2} :: * -> * -> *
+    roles nominal nominal
 COERCION AXIOMS
   axiom TypeFamilyInstanceLHS.D:R:FBool_1 :: F Bool _1 = Bool
   axiom TypeFamilyInstanceLHS.D:R:FInt_1 :: F Int _1 = Int
index 107f4aa..927ae6a 100644 (file)
@@ -2,6 +2,6 @@
 T14450.hs:33:3: error:
     • Type indexes must match class instance head
       Expected: Dom @k @k (IddSym0 @k)
-        Actual: Dom @* @* (IddSym0 @*) -- Defined at T14450.hs:33:8
+        Actual: Dom @* @* (IddSym0 @*)
     • In the type instance declaration for ‘Dom’
       In the instance declaration for ‘Varpi (IddSym0 :: k ~> k)’
index 4086c12..c2aa24d 100644 (file)
@@ -1,6 +1,6 @@
 TYPE CONSTRUCTORS
-  type role T nominal nominal representational nominal nominal
-  T{5} :: forall {k} k1. (k1 -> k -> *) -> k1 -> k -> *
+  data type T{5} :: forall {k} k1. (k1 -> k -> *) -> k1 -> k -> *
+    roles nominal nominal representational nominal nominal
 DATA CONSTRUCTORS
   MkT :: forall {k} k1 (f :: k1 -> k -> *) (a :: k1) (b :: k).
          f a b -> T f a b -> T f a b
index d07b3a1..6db525c 100644 (file)
@@ -1,7 +1,8 @@
 TYPE CONSTRUCTORS
-  C{2} :: forall {k}. k -> Constraint
-  type role T nominal nominal nominal nominal
-  T{4} :: forall k (f :: k -> *) (a :: k). f a -> *
+  class C{2} :: forall {k}. k -> Constraint
+  associated type family T{4} ::
+    forall k (f :: k -> *) (a :: k). f a -> *
+    roles nominal nominal nominal nominal
 Dependent modules: []
 Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
                      integer-gmp-1.0.2.0]
index 9ca6366..9e860d2 100644 (file)
@@ -2,6 +2,6 @@
 T15828.hs:9:3: error:
     • Type indexes must match class instance head
       Expected: T (Maybe a) _
-        Actual: T (Maybe a) b -- Defined at T15828.hs:9:20
+        Actual: T (Maybe a1) b
     • In the type instance declaration for ‘T’
       In the instance declaration for ‘C (Maybe a)’
index c2678b7..a54b9e9 100644 (file)
@@ -1,16 +1,16 @@
 TYPE CONSTRUCTORS
-  type role T1 nominal
-  T1{1} :: * -> *
-  T2{1} :: * -> *
-  type role T3 nominal phantom
-  T3{2} :: forall k. k -> *
-  type role T4 nominal nominal
-  T4{2} :: (* -> *) -> * -> *
-  T5{1} :: * -> *
-  type role T6 nominal phantom
-  T6{2} :: forall {k}. k -> *
-  type role T7 nominal phantom representational
-  T7{3} :: forall {k}. k -> * -> *
+  data type T1{1} :: * -> *
+    roles nominal
+  data type T2{1} :: * -> *
+  data type T3{2} :: forall k. k -> *
+    roles nominal phantom
+  data type T4{2} :: (* -> *) -> * -> *
+    roles nominal nominal
+  data type T5{1} :: * -> *
+  data type T6{2} :: forall {k}. k -> *
+    roles nominal phantom
+  data type T7{3} :: forall {k}. k -> * -> *
+    roles nominal phantom representational
 DATA CONSTRUCTORS
   K7 :: forall {k} (a :: k) b. b -> T7 a b
   K6 :: forall {k} (a :: k). T6 a
index 1745332..8df56e5 100644 (file)
@@ -1,8 +1,8 @@
 TYPE SIGNATURES
   meth2 :: forall a. C2 a => a -> a
 TYPE CONSTRUCTORS
-  type role C2 representational
-  C2{1} :: * -> Constraint
+  class C2{1} :: * -> Constraint
+    roles representational
 COERCION AXIOMS
   axiom Roles12.N:C2 :: C2 a = a -> a
 Dependent modules: []
index 1703151..425cc0c 100644 (file)
@@ -1,7 +1,7 @@
 TYPE CONSTRUCTORS
-  T1{1} :: * -> *
-  type role T2 phantom
-  T2{1} :: * -> *
+  data type T1{1} :: * -> *
+  data type T2{1} :: * -> *
+    roles phantom
 DATA CONSTRUCTORS
   K2 :: forall a. FunPtr a -> T2 a
   K1 :: forall a. IO a -> T1 a
index bf76b72..16fbdf0 100644 (file)
@@ -4,17 +4,17 @@ TYPE SIGNATURES
   meth3 :: forall a b. C3 a b => a -> F3 b -> F3 b
   meth4 :: forall a b. C4 a b => a -> F4 b -> F4 b
 TYPE CONSTRUCTORS
-  C1{1} :: * -> Constraint
-  C2{2} :: * -> * -> Constraint
-  C3{2} :: * -> * -> Constraint
-  C4{2} :: * -> * -> Constraint
-  type role F3 nominal
-  F3{1} :: * -> *
-  type role F4 nominal
-  F4{1} :: * -> *
-  type role Syn1 nominal
-  Syn1{1} :: * -> *
-  Syn2{1} :: * -> *
+  class C1{1} :: * -> Constraint
+  class C2{2} :: * -> * -> Constraint
+  class C3{2} :: * -> * -> Constraint
+  class C4{2} :: * -> * -> Constraint
+  associated type family F3{1} :: * -> *
+    roles nominal
+  type family F4{1} :: * -> *
+    roles nominal
+  type synonym Syn1{1} :: * -> *
+    roles nominal
+  type synonym Syn2{1} :: * -> *
 COERCION AXIOMS
   axiom Roles3.N:C1 :: C1 a = a -> a
   axiom Roles3.N:C2 :: C2 a b = (a ~ b) => a -> b
index dbca015..eb5d26a 100644 (file)
@@ -2,9 +2,9 @@ TYPE SIGNATURES
   meth1 :: forall a. C1 a => a -> a
   meth3 :: forall a. C3 a => a -> Syn1 a
 TYPE CONSTRUCTORS
-  C1{1} :: * -> Constraint
-  C3{1} :: * -> Constraint
-  Syn1{1} :: * -> *
+  class C1{1} :: * -> Constraint
+  class C3{1} :: * -> Constraint
+  type synonym Syn1{1} :: * -> *
 COERCION AXIOMS
   axiom Roles4.N:C1 :: C1 a = a -> a
   axiom Roles4.N:C3 :: C3 a = a -> Syn1 a
index 4e2fe00..930c05b 100644 (file)
@@ -2,11 +2,11 @@
 T8958.hs:1:31: warning:
     -XDatatypeContexts is deprecated: It was widely considered a misfeature, and has been removed from the Haskell language.
 TYPE CONSTRUCTORS
-  type role Map nominal representational
-  Map{2} :: * -> * -> *
-  Nominal{1} :: * -> Constraint
-  type role Representational representational
-  Representational{1} :: * -> Constraint
+  newtype Map{2} :: * -> * -> *
+    roles nominal representational
+  class Nominal{1} :: * -> Constraint
+  class Representational{1} :: * -> Constraint
+    roles representational
 COERCION AXIOMS
   axiom T8958.N:Map :: Map k v = [(k, v)]
 DATA CONSTRUCTORS
index 3807609..2970df6 100644 (file)
@@ -1,6 +1,6 @@
 TYPE CONSTRUCTORS
-  type role T nominal representational
-  T{2} :: forall k. k -> *
+  data type T{2} :: forall k. k -> *
+    roles nominal representational
 Dependent modules: []
 Dependent packages: [array-0.5.2.0, base-4.12.0.0, deepseq-1.4.4.0,
                      ghc-boot-th-8.7, ghc-prim-0.5.3, integer-gmp-1.0.2.0,
index 99a66bd..eff7c0a 100644 (file)
@@ -2,7 +2,7 @@ TYPE SIGNATURES
   f :: Int -> ()
   m :: forall a. C a => a -> ()
 TYPE CONSTRUCTORS
-  C{1} :: * -> Constraint
+  class C{1} :: * -> Constraint
 COERCION AXIOMS
   axiom T12763.N:C :: C a = a -> ()
 CLASS INSTANCES
index 18beabd..8340d3f 100644 (file)
@@ -6,9 +6,9 @@ TYPE SIGNATURES
   huh :: forall s a b chain. Zork s a b => Q s a chain -> ST s ()
   s :: forall t t1. Q t (Z [Char]) t1 -> Q t (Z [Char]) t1
 TYPE CONSTRUCTORS
-  Q{3} :: * -> * -> * -> *
-  Z{1} :: * -> *
-  Zork{3} :: * -> * -> * -> Constraint
+  data type Q{3} :: * -> * -> * -> *
+  data type Z{1} :: * -> *
+  class Zork{3} :: * -> * -> * -> Constraint
 COERCION AXIOMS
   axiom N:Zork :: Zork s a b = forall chain. Q s a chain -> ST s ()
 DATA CONSTRUCTORS