Commit 1c353623 authored by Ryan Scott's avatar Ryan Scott

Use IfaceAppArgs to store an IfaceAppTy's arguments

Summary:
Currently, an `IfaceAppTy` has no way to tell whether its
argument is visible or not, so it simply treats all arguments as
visible, leading to #15330. We already have a solution for this
problem in the form of the `IfaceTcArgs` data structure, used by
`IfaceTyConApp` to represent the arguments to a type constructor.
Therefore, it makes sense to reuse this machinery for `IfaceAppTy`,
so this patch does just that.

This patch:

1. Renames `IfaceTcArgs` to `IfaceAppArgs` to reflect its more
   general purpose.
2. Changes the second field of `IfaceAppTy` from `IfaceType` to
   `IfaceAppArgs`, and propagates the necessary changes through. In
   particular, pretty-printing an `IfaceAppTy` now goes through the
   `IfaceAppArgs` pretty-printer, which correctly displays arguments
   as visible or not for free, fixing #15330.
3. Changes `toIfaceTypeX` and related functions so that when
   converting an `AppTy` to an `IfaceAppTy`, it flattens as many
   argument `AppTy`s as possible, and then converts those arguments
   into an `IfaceAppArgs` list, using the kind of the function
   `Type` as a guide. (Doing so minimizes the number of times we need
   to call `typeKind`, which is more expensive that finding the kind
   of a `TyCon`.)

Test Plan: make test TEST=T15330

Reviewers: goldfire, simonpj, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #15330

Differential Revision: https://phabricator.haskell.org/D4938
parent e24da5ed
......@@ -512,7 +512,7 @@ rnIfaceTyConParent :: Rename IfaceTyConParent
rnIfaceTyConParent (IfDataInstance n tc args)
= IfDataInstance <$> rnIfaceGlobal n
<*> rnIfaceTyCon tc
<*> rnIfaceTcArgs args
<*> rnIfaceAppArgs args
rnIfaceTyConParent IfNoParent = pure IfNoParent
rnIfaceConDecls :: Rename IfaceConDecls
......@@ -557,7 +557,7 @@ rnMaybeDefMethSpec mb = return mb
rnIfaceAxBranch :: Rename IfaceAxBranch
rnIfaceAxBranch d = do
ty_vars <- mapM rnIfaceTvBndr (ifaxbTyVars d)
lhs <- rnIfaceTcArgs (ifaxbLHS d)
lhs <- rnIfaceAppArgs (ifaxbLHS d)
rhs <- rnIfaceType (ifaxbRHS d)
return d { ifaxbTyVars = ty_vars
, ifaxbLHS = lhs
......@@ -693,16 +693,16 @@ rnIfaceType :: Rename IfaceType
rnIfaceType (IfaceFreeTyVar n) = pure (IfaceFreeTyVar n)
rnIfaceType (IfaceTyVar n) = pure (IfaceTyVar n)
rnIfaceType (IfaceAppTy t1 t2)
= IfaceAppTy <$> rnIfaceType t1 <*> rnIfaceType t2
= IfaceAppTy <$> rnIfaceType t1 <*> rnIfaceAppArgs t2
rnIfaceType (IfaceLitTy l) = return (IfaceLitTy l)
rnIfaceType (IfaceFunTy t1 t2)
= IfaceFunTy <$> rnIfaceType t1 <*> rnIfaceType t2
rnIfaceType (IfaceDFunTy t1 t2)
= IfaceDFunTy <$> rnIfaceType t1 <*> rnIfaceType t2
rnIfaceType (IfaceTupleTy s i tks)
= IfaceTupleTy s i <$> rnIfaceTcArgs tks
= IfaceTupleTy s i <$> rnIfaceAppArgs tks
rnIfaceType (IfaceTyConApp tc tks)
= IfaceTyConApp <$> rnIfaceTyCon tc <*> rnIfaceTcArgs tks
= IfaceTyConApp <$> rnIfaceTyCon tc <*> rnIfaceAppArgs tks
rnIfaceType (IfaceForAllTy tv t)
= IfaceForAllTy <$> rnIfaceForAllBndr tv <*> rnIfaceType t
rnIfaceType (IfaceCoercionTy co)
......@@ -713,7 +713,7 @@ rnIfaceType (IfaceCastTy ty co)
rnIfaceForAllBndr :: Rename IfaceForAllBndr
rnIfaceForAllBndr (TvBndr tv vis) = TvBndr <$> rnIfaceTvBndr tv <*> pure vis
rnIfaceTcArgs :: Rename IfaceTcArgs
rnIfaceTcArgs (ITC_Invis t ts) = ITC_Invis <$> rnIfaceType t <*> rnIfaceTcArgs ts
rnIfaceTcArgs (ITC_Vis t ts) = ITC_Vis <$> rnIfaceType t <*> rnIfaceTcArgs ts
rnIfaceTcArgs ITC_Nil = pure ITC_Nil
rnIfaceAppArgs :: Rename IfaceAppArgs
rnIfaceAppArgs (IA_Invis t ts) = IA_Invis <$> rnIfaceType t <*> rnIfaceAppArgs ts
rnIfaceAppArgs (IA_Vis t ts) = IA_Vis <$> rnIfaceType t <*> rnIfaceAppArgs ts
rnIfaceAppArgs IA_Nil = pure IA_Nil
......@@ -184,7 +184,7 @@ data IfaceTyConParent
= IfNoParent
| IfDataInstance IfExtName
IfaceTyCon
IfaceTcArgs
IfaceAppArgs
data IfaceFamTyConFlav
= IfaceDataFamilyTyCon -- Data family
......@@ -211,7 +211,7 @@ data IfaceAT = IfaceAT -- See Class.ClassATItem
-- This is just like CoAxBranch
data IfaceAxBranch = IfaceAxBranch { ifaxbTyVars :: [IfaceTvBndr]
, ifaxbCoVars :: [IfaceIdBndr]
, ifaxbLHS :: IfaceTcArgs
, ifaxbLHS :: IfaceAppArgs
, ifaxbRoles :: [Role]
, ifaxbRHS :: IfaceType
, ifaxbIncomps :: [BranchIndex] }
......@@ -573,7 +573,7 @@ pprAxBranch pp_tc (IfaceAxBranch { ifaxbTyVars = tvs
| otherwise
= brackets (pprWithCommas (pprIfaceTvBndr True) tvs <> semi <+>
pprWithCommas pprIfaceIdBndr cvs)
pp_lhs = hang pp_tc 2 (pprParendIfaceTcArgs pat_tys)
pp_lhs = hang pp_tc 2 (pprParendIfaceAppArgs pat_tys)
maybe_incomps = ppUnless (null incomps) $ parens $
text "incompatible indices:" <+> ppr incomps
......@@ -1050,7 +1050,7 @@ pprIfaceConDecl ss gadt_style tycon tc_binders parent
-- See Note [Result type of a data family GADT]
mk_user_con_res_ty eq_spec
| IfDataInstance _ tc tys <- parent
= pprIfaceType (IfaceTyConApp tc (substIfaceTcArgs gadt_subst tys))
= pprIfaceType (IfaceTyConApp tc (substIfaceAppArgs gadt_subst tys))
| otherwise
= sdocWithDynFlags (ppr_tc_app gadt_subst)
where
......@@ -1347,7 +1347,7 @@ freeNamesIfAxBranch (IfaceAxBranch { ifaxbTyVars = tyvars
, ifaxbRHS = rhs })
= fnList freeNamesIfTvBndr tyvars &&&
fnList freeNamesIfIdBndr covars &&&
freeNamesIfTcArgs lhs &&&
freeNamesIfAppArgs lhs &&&
freeNamesIfType rhs
freeNamesIfIdDetails :: IfaceIdDetails -> NameSet
......@@ -1407,17 +1407,17 @@ freeNamesIfBang _ = emptyNameSet
freeNamesIfKind :: IfaceType -> NameSet
freeNamesIfKind = freeNamesIfType
freeNamesIfTcArgs :: IfaceTcArgs -> NameSet
freeNamesIfTcArgs (ITC_Vis t ts) = freeNamesIfType t &&& freeNamesIfTcArgs ts
freeNamesIfTcArgs (ITC_Invis k ks) = freeNamesIfKind k &&& freeNamesIfTcArgs ks
freeNamesIfTcArgs ITC_Nil = emptyNameSet
freeNamesIfAppArgs :: IfaceAppArgs -> NameSet
freeNamesIfAppArgs (IA_Vis t ts) = freeNamesIfType t &&& freeNamesIfAppArgs ts
freeNamesIfAppArgs (IA_Invis k ks) = freeNamesIfKind k &&& freeNamesIfAppArgs ks
freeNamesIfAppArgs IA_Nil = emptyNameSet
freeNamesIfType :: IfaceType -> NameSet
freeNamesIfType (IfaceFreeTyVar _) = emptyNameSet
freeNamesIfType (IfaceTyVar _) = emptyNameSet
freeNamesIfType (IfaceAppTy s t) = freeNamesIfType s &&& freeNamesIfType t
freeNamesIfType (IfaceTyConApp tc ts) = freeNamesIfTc tc &&& freeNamesIfTcArgs ts
freeNamesIfType (IfaceTupleTy _ _ ts) = freeNamesIfTcArgs ts
freeNamesIfType (IfaceAppTy s t) = freeNamesIfType s &&& freeNamesIfAppArgs t
freeNamesIfType (IfaceTyConApp tc ts) = freeNamesIfTc tc &&& freeNamesIfAppArgs ts
freeNamesIfType (IfaceTupleTy _ _ ts) = freeNamesIfAppArgs ts
freeNamesIfType (IfaceLitTy _) = emptyNameSet
freeNamesIfType (IfaceForAllTy tv t) = freeNamesIfTyVarBndr tv &&& freeNamesIfType t
freeNamesIfType (IfaceFunTy s t) = freeNamesIfType s &&& freeNamesIfType t
......@@ -1567,7 +1567,7 @@ freeNamesIfFamInst (IfaceFamInst { ifFamInstFam = famName
freeNamesIfaceTyConParent :: IfaceTyConParent -> NameSet
freeNamesIfaceTyConParent IfNoParent = emptyNameSet
freeNamesIfaceTyConParent (IfDataInstance ax tc tys)
= unitNameSet ax &&& freeNamesIfTc tc &&& freeNamesIfTcArgs tys
= unitNameSet ax &&& freeNamesIfTc tc &&& freeNamesIfAppArgs tys
-- helpers
(&&&) :: NameSet -> NameSet -> NameSet
......
This diff is collapsed.
-- Used only by ToIface.hs-boot
module IfaceType( IfaceType, IfaceTyCon, IfaceForAllBndr
, IfaceCoercion, IfaceTyLit, IfaceTcArgs ) where
, IfaceCoercion, IfaceTyLit, IfaceAppArgs ) where
import Var (TyVarBndr, ArgFlag)
import FastString (FastString)
data IfaceTcArgs
data IfaceAppArgs
type IfLclName = FastString
type IfaceKind = IfaceType
......
......@@ -670,7 +670,7 @@ tc_iface_decl _ _ (IfaceData {ifName = tc_name,
= do { ax <- tcIfaceCoAxiom ax_name
; let fam_tc = coAxiomTyCon ax
ax_unbr = toUnbranchedAxiom ax
; lhs_tys <- tcIfaceTcArgs arg_tys
; lhs_tys <- tcIfaceAppArgs arg_tys
; return (DataFamInstTyCon ax_unbr fam_tc lhs_tys) }
tc_iface_decl _ _ (IfaceSynonym {ifName = tc_name,
......@@ -865,7 +865,7 @@ tc_ax_branch prev_branches
(map (\b -> TvBndr b (NamedTCB Inferred)) tv_bndrs) $ \ tvs ->
-- The _AT variant is needed here; see Note [CoAxBranch type variables] in CoAxiom
bindIfaceIds cv_bndrs $ \ cvs -> do
{ tc_lhs <- tcIfaceTcArgs lhs
{ tc_lhs <- tcIfaceAppArgs lhs
; tc_rhs <- tcIfaceType rhs
; let br = CoAxBranch { cab_loc = noSrcSpan
, cab_tvs = binderVars tvs
......@@ -1074,7 +1074,7 @@ tcIfaceRule (IfaceRule {ifRuleName = name, ifActivation = act, ifRuleBndrs = bnd
-- to write them out in coreRuleToIfaceRule
ifTopFreeName :: IfaceExpr -> Maybe Name
ifTopFreeName (IfaceType (IfaceTyConApp tc _ )) = Just (ifaceTyConName tc)
ifTopFreeName (IfaceType (IfaceTupleTy s _ ts)) = Just (tupleTyConName s (length (tcArgsIfaceTypes ts)))
ifTopFreeName (IfaceType (IfaceTupleTy s _ ts)) = Just (tupleTyConName s (length (appArgsIfaceTypes ts)))
ifTopFreeName (IfaceApp f _) = ifTopFreeName f
ifTopFreeName (IfaceExt n) = Just n
ifTopFreeName _ = Nothing
......@@ -1132,14 +1132,17 @@ tcIfaceType = go
where
go (IfaceTyVar n) = TyVarTy <$> tcIfaceTyVar n
go (IfaceFreeTyVar n) = pprPanic "tcIfaceType:IfaceFreeTyVar" (ppr n)
go (IfaceAppTy t1 t2) = AppTy <$> go t1 <*> go t2
go (IfaceLitTy l) = LitTy <$> tcIfaceTyLit l
go (IfaceFunTy t1 t2) = FunTy <$> go t1 <*> go t2
go (IfaceDFunTy t1 t2) = FunTy <$> go t1 <*> go t2
go (IfaceTupleTy s i tks) = tcIfaceTupleTy s i tks
go (IfaceAppTy t ts)
= do { t' <- go t
; ts' <- traverse go (appArgsIfaceTypes ts)
; pure (foldl' AppTy t' ts') }
go (IfaceTyConApp tc tks)
= do { tc' <- tcIfaceTyCon tc
; tks' <- mapM go (tcArgsIfaceTypes tks)
; tks' <- mapM go (appArgsIfaceTypes tks)
; return (mkTyConApp tc' tks') }
go (IfaceForAllTy bndr t)
= bindIfaceForAllBndr bndr $ \ tv' vis ->
......@@ -1147,9 +1150,9 @@ tcIfaceType = go
go (IfaceCastTy ty co) = CastTy <$> go ty <*> tcIfaceCo co
go (IfaceCoercionTy co) = CoercionTy <$> tcIfaceCo co
tcIfaceTupleTy :: TupleSort -> IsPromoted -> IfaceTcArgs -> IfL Type
tcIfaceTupleTy :: TupleSort -> IsPromoted -> IfaceAppArgs -> IfL Type
tcIfaceTupleTy sort is_promoted args
= do { args' <- tcIfaceTcArgs args
= do { args' <- tcIfaceAppArgs args
; let arity = length args'
; base_tc <- tcTupleTyCon True sort arity
; case is_promoted of
......@@ -1176,8 +1179,8 @@ tcTupleTyCon in_type sort arity
| otherwise = arity
-- in expressions, we only have term args
tcIfaceTcArgs :: IfaceTcArgs -> IfL [Type]
tcIfaceTcArgs = mapM tcIfaceType . tcArgsIfaceTypes
tcIfaceAppArgs :: IfaceAppArgs -> IfL [Type]
tcIfaceAppArgs = mapM tcIfaceType . appArgsIfaceTypes
-----------------------------------------
tcIfaceCtxt :: IfaceContext -> IfL ThetaType
......
......@@ -122,7 +122,12 @@ toIfaceTypeX :: VarSet -> Type -> IfaceType
toIfaceTypeX fr (TyVarTy tv) -- See Note [TcTyVars in IfaceType] in IfaceType
| tv `elemVarSet` fr = IfaceFreeTyVar tv
| otherwise = IfaceTyVar (toIfaceTyVar tv)
toIfaceTypeX fr (AppTy t1 t2) = IfaceAppTy (toIfaceTypeX fr t1) (toIfaceTypeX fr t2)
toIfaceTypeX fr ty@(AppTy {}) =
-- Flatten as many argument AppTys as possible, then turn them into an
-- IfaceAppArgs list.
-- See Note [Suppressing invisible arguments] in IfaceType.
let (head, args) = splitAppTys ty
in IfaceAppTy (toIfaceTypeX fr head) (toIfaceAppTyArgsX fr head args)
toIfaceTypeX _ (LitTy n) = IfaceLitTy (toIfaceTyLit n)
toIfaceTypeX fr (ForAllTy b t) = IfaceForAllTy (toIfaceForAllBndrX fr b)
(toIfaceTypeX (fr `delVarSet` binderVar b) t)
......@@ -263,11 +268,17 @@ toIfaceCoercionX fr co
go_prov (ProofIrrelProv co) = IfaceProofIrrelProv (go co)
go_prov (PluginProv str) = IfacePluginProv str
toIfaceTcArgs :: TyCon -> [Type] -> IfaceTcArgs
toIfaceTcArgs :: TyCon -> [Type] -> IfaceAppArgs
toIfaceTcArgs = toIfaceTcArgsX emptyVarSet
toIfaceTcArgsX :: VarSet -> TyCon -> [Type] -> IfaceTcArgs
-- See Note [Suppressing invisible arguments]
toIfaceTcArgsX :: VarSet -> TyCon -> [Type] -> IfaceAppArgs
toIfaceTcArgsX fr tc ty_args = toIfaceAppArgsX fr (tyConKind tc) ty_args
toIfaceAppTyArgsX :: VarSet -> Type -> [Type] -> IfaceAppArgs
toIfaceAppTyArgsX fr ty ty_args = toIfaceAppArgsX fr (typeKind ty) ty_args
toIfaceAppArgsX :: VarSet -> Kind -> [Type] -> IfaceAppArgs
-- See Note [Suppressing invisible arguments] in IfaceType
-- We produce a result list of args describing visibility
-- The awkward case is
-- T :: forall k. * -> k
......@@ -275,34 +286,34 @@ toIfaceTcArgsX :: VarSet -> TyCon -> [Type] -> IfaceTcArgs
-- T (forall j. blah) * blib
-- Is 'blib' visible? It depends on the visibility flag on j,
-- so we have to substitute for k. Annoying!
toIfaceTcArgsX fr tc ty_args
= go (mkEmptyTCvSubst in_scope) (tyConKind tc) ty_args
toIfaceAppArgsX fr kind ty_args
= go (mkEmptyTCvSubst in_scope) kind ty_args
where
in_scope = mkInScopeSet (tyCoVarsOfTypes ty_args)
go _ _ [] = ITC_Nil
go _ _ [] = IA_Nil
go env ty ts
| Just ty' <- coreView ty
= go env ty' ts
go env (ForAllTy (TvBndr tv vis) res) (t:ts)
| isVisibleArgFlag vis = ITC_Vis t' ts'
| otherwise = ITC_Invis t' ts'
| isVisibleArgFlag vis = IA_Vis t' ts'
| otherwise = IA_Invis t' ts'
where
t' = toIfaceTypeX fr t
ts' = go (extendTvSubst env tv t) res ts
go env (FunTy _ res) (t:ts) -- No type-class args in tycon apps
= ITC_Vis (toIfaceTypeX fr t) (go env res ts)
= IA_Vis (toIfaceTypeX fr t) (go env res ts)
go env (TyVarTy tv) ts
| Just ki <- lookupTyVar env tv = go env ki ts
go env kind (t:ts) = WARN( True, ppr tc $$ ppr (tyConKind tc) $$ ppr ty_args )
ITC_Vis (toIfaceTypeX fr t) (go env kind ts) -- Ill-kinded
go env kind (t:ts) = WARN( True, ppr kind $$ ppr ty_args )
IA_Vis (toIfaceTypeX fr t) (go env kind ts) -- Ill-kinded
tidyToIfaceType :: TidyEnv -> Type -> IfaceType
tidyToIfaceType env ty = toIfaceType (tidyType env ty)
tidyToIfaceTcArgs :: TidyEnv -> TyCon -> [Type] -> IfaceTcArgs
tidyToIfaceTcArgs :: TidyEnv -> TyCon -> [Type] -> IfaceAppArgs
tidyToIfaceTcArgs env tc tys = toIfaceTcArgs tc (tidyTypes env tys)
tidyToIfaceContext :: TidyEnv -> ThetaType -> IfaceContext
......
......@@ -2,7 +2,7 @@ module ToIface where
import {-# SOURCE #-} TyCoRep
import {-# SOURCE #-} IfaceType( IfaceType, IfaceTyCon, IfaceForAllBndr
, IfaceCoercion, IfaceTyLit, IfaceTcArgs )
, IfaceCoercion, IfaceTyLit, IfaceAppArgs )
import Var ( TyVarBinder )
import TyCon ( TyCon )
import VarSet( VarSet )
......@@ -12,5 +12,5 @@ toIfaceTypeX :: VarSet -> Type -> IfaceType
toIfaceTyLit :: TyLit -> IfaceTyLit
toIfaceForAllBndr :: TyVarBinder -> IfaceForAllBndr
toIfaceTyCon :: TyCon -> IfaceTyCon
toIfaceTcArgs :: TyCon -> [Type] -> IfaceTcArgs
toIfaceTcArgs :: TyCon -> [Type] -> IfaceAppArgs
toIfaceCoercionX :: VarSet -> Coercion -> IfaceCoercion
......@@ -2693,6 +2693,9 @@ defined to use this. @pprParendType@ is the same, except it puts
parens around the type, except for the atomic cases. @pprParendType@
works just by setting the initial context precedence very high.
Note that any function which pretty-prints a @Type@ first converts the @Type@
to an @IfaceType@. See Note [IfaceType and pretty-printing] in IfaceType.
See Note [Precedence in types] in BasicTypes.
-}
......
T14369.hs:27:5: error:
• Couldn't match type ‘Demote a’ with ‘Demote a1’
Expected type: Sing (x a) -> Maybe (Demote a1)
Actual type: Sing (x a) -> Demote (Maybe a)
Expected type: Sing x -> Maybe (Demote a1)
Actual type: Sing x -> Demote (Maybe a)
• In the expression: fromSing
In an equation for ‘f’: f = fromSing
• Relevant bindings include
f :: Sing (x a) -> Maybe (Demote a1) (bound at T14369.hs:27:1)
f :: Sing x -> Maybe (Demote a1) (bound at T14369.hs:27:1)
T14040a.hs:34:8: error:
• Cannot apply expression of type ‘Sing wl
-> (forall y. p k0 w0 'WeirdNil)
-> (forall y. p w0 'WeirdNil)
-> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
Sing x
-> Sing xs
-> p (WeirdList k1) w1 xs
-> p k1 w2 ('WeirdCons x xs))
-> p k2 w3 wl’
Sing x -> Sing xs -> p w1 xs -> p w2 ('WeirdCons x xs))
-> p w3 wl’
to a visible type argument ‘(WeirdList z)’
• In the sixth argument of ‘pWeirdCons’, namely
‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
......
T14350.hs:59:15: error:
• Couldn't match expected type ‘Proxy a2
-> Apply (Apply (c x3) 'Proxy) (Apply (g x3) 'Proxy)’
with actual type ‘Sing (f x y @@ t0)’
-> Apply (Apply c 'Proxy) (Apply g 'Proxy)’
with actual type ‘Sing (f @@ t0)’
• The function ‘applySing’ is applied to three arguments,
but its type ‘Sing (f x y) -> Sing t0 -> Sing (f x y @@ t0)’
has only two
but its type ‘Sing f -> Sing t0 -> Sing (f @@ t0)’ has only two
In the expression: applySing f Proxy Proxy
In an equation for ‘dcomp’: dcomp f g x = applySing f Proxy Proxy
• Relevant bindings include
x :: Sing x3 (bound at T14350.hs:59:11)
g :: Sing (g x2) (bound at T14350.hs:59:9)
f :: Sing (f x1 y) (bound at T14350.hs:59:7)
dcomp :: Sing (f x1 y)
-> Sing (g x2) -> Sing x3 -> (c x3 @@ 'Proxy) @@ (g x3 @@ 'Proxy)
g :: Sing g (bound at T14350.hs:59:9)
f :: Sing f (bound at T14350.hs:59:7)
dcomp :: Sing f
-> Sing g -> Sing x3 -> (c @@ 'Proxy) @@ (g @@ 'Proxy)
(bound at T14350.hs:59:1)
T14350.hs:59:27: error:
......@@ -24,8 +23,8 @@ T14350.hs:59:27: error:
In an equation for ‘dcomp’: dcomp f g x = applySing f Proxy Proxy
• Relevant bindings include
x :: Sing x3 (bound at T14350.hs:59:11)
g :: Sing (g x2) (bound at T14350.hs:59:9)
f :: Sing (f x1 y) (bound at T14350.hs:59:7)
dcomp :: Sing (f x1 y)
-> Sing (g x2) -> Sing x3 -> (c x3 @@ 'Proxy) @@ (g x3 @@ 'Proxy)
g :: Sing g (bound at T14350.hs:59:9)
f :: Sing f (bound at T14350.hs:59:7)
dcomp :: Sing f
-> Sing g -> Sing x3 -> (c @@ 'Proxy) @@ (g @@ 'Proxy)
(bound at T14350.hs:59:1)
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
module T15330 where
import Data.Kind
import Data.Proxy
data T :: forall a. a -> Type
f1 :: Proxy (T True)
f1 = "foo"
f2 :: forall (t :: forall a. a -> Type).
Proxy (t True)
f2 = "foo"
T15330.hs:11:6: error:
• Couldn't match expected type ‘Proxy (T 'True)’
with actual type ‘[Char]’
• In the expression: "foo"
In an equation for ‘f1’: f1 = "foo"
T15330.hs:15:6: error:
• Couldn't match expected type ‘Proxy (t 'True)’
with actual type ‘[Char]’
• In the expression: "foo"
In an equation for ‘f2’: f2 = "foo"
• Relevant bindings include
f2 :: Proxy (t 'True) (bound at T15330.hs:15:1)
......@@ -474,3 +474,4 @@ test('T14884', normal, compile_fail, [''])
test('T14904a', normal, compile_fail, [''])
test('T14904b', normal, compile_fail, [''])
test('T15067', normal, compile_fail, [''])
test('T15330', normal, compile_fail, [''])
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment