Commit 5b7ca039 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Wibble to Taming the Kind Inference Monster

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.
parent eee1b61f
......@@ -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]
}
......
......@@ -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)
......
......@@ -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
......
......@@ -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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
......@@ -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')
......
......@@ -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
......
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]
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)
......
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]
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]
......@@ -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
......
......@@ -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’
......
......@@ -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’
......
......@@ -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)’
......@@ -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)’
......@@ -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’
......@@ -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)’
......@@ -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 :: *)’
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: []
......
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]
......@@ -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)
......
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,
......
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: []
......
......@@ -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: []
......
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
......
......@@ -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)’
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
......
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]
......@@ -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)’
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
......
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: []
......
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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
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,
......
......@@ -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
......
......@@ -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} :: * -> * -> * -> *