Fix #13337.
authorRichard Eisenberg <rae@cs.brynmawr.edu>
Tue, 14 Mar 2017 17:32:00 +0000 (13:32 -0400)
committerBen Gamari <ben@smart-cactus.org>
Tue, 14 Mar 2017 19:10:36 +0000 (15:10 -0400)
The big change is the introduction of solveSomeEqualities. This
is just like solveEqualities, but it doesn't fail if there are unsolved
equalities when it's all done. Anything unsolved is re-emitted. This
is appropriate if we are not kind-generalizing, so this new form
is used when decideKindGeneralizationPlan says not to.

We initially thought that any use of solveEqualities would be tied
to kind generalization, but this isn't true. For example, we need
to solveEqualities a bunch in the "tc" pass in TcTyClsDecls (which
is really desugaring). These equalities are all surely going to be
soluble (if they weren't the "kc" pass would fail), but we still
need to solve them again. Perhaps if the "kc" pass produced type-
checked output that is then desugared, solveEqualities really would
be tied only to kind generalization.

Updates haddock submodule.

Test Plan: ./validate, typecheck/should_compile/T13337

Reviewers: simonpj, bgamari, austin

Reviewed By: simonpj

Subscribers: RyanGlScott, rwbarton, thomie

Differential Revision: https://phabricator.haskell.org/D3315

17 files changed:
compiler/hsSyn/Convert.hs
compiler/hsSyn/HsDecls.hs
compiler/hsSyn/HsTypes.hs
compiler/rename/RnSource.hs
compiler/rename/RnTypes.hs
compiler/typecheck/TcBinds.hs
compiler/typecheck/TcForeign.hs
compiler/typecheck/TcHsType.hs
compiler/typecheck/TcSimplify.hs
compiler/typecheck/TcTyClsDecls.hs
testsuite/tests/parser/should_compile/DumpParsedAst.stderr
testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
testsuite/tests/partial-sigs/should_fail/T11976.stderr
testsuite/tests/partial-sigs/should_fail/T12634.stderr
testsuite/tests/typecheck/should_compile/T13337.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/all.T
utils/haddock

index 7e786bd..921448e 100644 (file)
@@ -513,7 +513,7 @@ cvtConstr (ForallC tvs ctxt con)
                   let hs_ty  = mkHsForAllTy tvs noSrcSpan tvs' rho_ty
                       rho_ty = mkHsQualTy ctxt noSrcSpan (L loc ctxt')
                                                          (hsib_body conT)
-                  in con' { con_type = HsIB PlaceHolder hs_ty }
+                  in con' { con_type = mkHsImplicitBndrs hs_ty }
                 ConDeclH98  {} ->
                   let qvars = case (tvs, con_qvars con') of
                         ([], Nothing) -> Nothing
index e3029a2..8634432 100644 (file)
@@ -1088,7 +1088,7 @@ instance (OutputableBndrId name)
         -- This complexity is to distinguish between
         --    deriving Show
         --    deriving (Show)
-        pp_dct [a@(HsIB _ (L _ HsAppsTy{}))] = parens (ppr a)
+        pp_dct [a@(HsIB { hsib_body = L _ HsAppsTy{} })] = parens (ppr a)
         pp_dct [a] = ppr a
         pp_dct _   = parens (interpp'SP dct)
 
index 998f8bd..8ea6b0b 100644 (file)
@@ -290,6 +290,9 @@ isEmptyLHsQTvs _                = False
 data HsImplicitBndrs name thing   -- See Note [HsType binders]
   = HsIB { hsib_vars :: PostRn name [Name] -- Implicitly-bound kind & type vars
          , hsib_body :: thing              -- Main payload (type or list of types)
+         , hsib_closed :: PostRn name Bool -- Taking the hsib_vars into account,
+                                           -- is the payload closed? Used in
+                                           -- TcHsType.decideKindGeneralisationPlan
     }
 
 -- | Haskell Wildcard Binders
@@ -306,7 +309,7 @@ data HsWildCardBndrs name thing
                 -- it's still there in the hsc_body.
     }
 
-deriving instance (Data name, Data thing, Data (PostRn name [Name]))
+deriving instance (Data name, Data thing, Data (PostRn name [Name]), Data (PostRn name Bool))
   => Data (HsImplicitBndrs name thing)
 
 deriving instance (Data name, Data thing, Data (PostRn name [Name]))
@@ -357,8 +360,9 @@ the explicitly forall'd tyvar 'a' is bound by the HsForAllTy
 -}
 
 mkHsImplicitBndrs :: thing -> HsImplicitBndrs RdrName thing
-mkHsImplicitBndrs x = HsIB { hsib_body = x
-                           , hsib_vars = PlaceHolder }
+mkHsImplicitBndrs x = HsIB { hsib_body   = x
+                           , hsib_vars   = PlaceHolder
+                           , hsib_closed = PlaceHolder }
 
 mkHsWildCardBndrs :: thing -> HsWildCardBndrs RdrName thing
 mkHsWildCardBndrs x = HsWC { hswc_body = x
@@ -367,8 +371,9 @@ mkHsWildCardBndrs x = HsWC { hswc_body = x
 -- Add empty binders.  This is a bit suspicious; what if
 -- the wrapped thing had free type variables?
 mkEmptyImplicitBndrs :: thing -> HsImplicitBndrs Name thing
-mkEmptyImplicitBndrs x = HsIB { hsib_body = x
-                              , hsib_vars = [] }
+mkEmptyImplicitBndrs x = HsIB { hsib_body   = x
+                              , hsib_vars   = []
+                              , hsib_closed = False }
 
 mkEmptyWildCardBndrs :: thing -> HsWildCardBndrs Name thing
 mkEmptyWildCardBndrs x = HsWC { hswc_body = x
index 601d45b..30915d5 100644 (file)
@@ -777,7 +777,8 @@ rnFamInstDecl doc mb_cls tycon (HsIB { hsib_body = pats }) payload rnPayload
 
        ; return (tycon',
                  HsIB { hsib_body = pats'
-                      , hsib_vars = all_ibs },
+                      , hsib_vars = all_ibs
+                      , hsib_closed = True },
                  payload',
                  all_fvs) }
              -- type instance => use, hence addOneFV
index b740647..74e6b52 100644 (file)
@@ -110,7 +110,7 @@ rn_hs_sig_wc_type no_implicit_if_forall ctxt
        ; rnImplicitBndrs no_implicit_if_forall tv_rdrs hs_ty $ \ vars ->
     do { (wcs, hs_ty', fvs1) <- rnWcBody ctxt nwc_rdrs hs_ty
        ; let sig_ty' = HsWC { hswc_wcs = wcs, hswc_body = ib_ty' }
-             ib_ty'  = HsIB { hsib_vars = vars, hsib_body = hs_ty' }
+             ib_ty'  = mk_implicit_bndrs vars hs_ty' fvs1
        ; (res, fvs2) <- thing_inside sig_ty'
        ; return (res, fvs1 `plusFV` fvs2) } }
 
@@ -247,8 +247,7 @@ rnHsSigType ctx (HsIB { hsib_body = hs_ty })
   = do { vars <- extractFilteredRdrTyVars hs_ty
        ; rnImplicitBndrs True vars hs_ty $ \ vars ->
     do { (body', fvs) <- rnLHsType ctx hs_ty
-       ; return (HsIB { hsib_vars = vars
-                      , hsib_body = body' }, fvs) } }
+       ; return ( mk_implicit_bndrs vars body' fvs, fvs ) } }
 
 rnImplicitBndrs :: Bool    -- True <=> no implicit quantification
                            --          if type is headed by a forall
@@ -292,6 +291,15 @@ rnLHsInstType doc_str inst_ty
          text "Malformed instance:" <+> ppr inst_ty
        ; rnHsSigType (GenericCtx doc_str) inst_ty }
 
+mk_implicit_bndrs :: [Name]      -- implicitly bound
+                  -> a           -- payload
+                  -> FreeVars    -- FreeVars of payload
+                  -> HsImplicitBndrs Name a
+mk_implicit_bndrs vars body fvs
+  = HsIB { hsib_vars = vars
+         , hsib_body = body
+         , hsib_closed = nameSetAll (not . isTyVarName) (vars `delFVs` fvs) }
+
 
 {- ******************************************************
 *                                                       *
index eef20a2..0f381c4 100644 (file)
@@ -321,8 +321,7 @@ tcHsBootSigs binds sigs
     tc_boot_sig (TypeSig lnames hs_ty) = mapM f lnames
       where
         f (L _ name)
-          = do { sigma_ty <- solveEqualities $
-                             tcHsSigWcType (FunSigCtxt name False) hs_ty
+          = do { sigma_ty <- tcHsSigWcType (FunSigCtxt name False) hs_ty
                ; return (mkVanillaGlobal name sigma_ty) }
         -- Notice that we make GlobalIds, not LocalIds
     tc_boot_sig s = pprPanic "tcHsBootSigs/tc_boot_sig" (ppr s)
index aef1e9c..1c54b1b 100644 (file)
@@ -240,7 +240,7 @@ tcFImport :: LForeignDecl Name -> TcM (Id, LForeignDecl Id, Bag GlobalRdrElt)
 tcFImport (L dloc fo@(ForeignImport { fd_name = L nloc nm, fd_sig_ty = hs_ty
                                     , fd_fi = imp_decl }))
   = setSrcSpan dloc $ addErrCtxt (foreignDeclCtxt fo)  $
-    do { sig_ty <- solveEqualities $ tcHsSigType (ForSigCtxt nm) hs_ty
+    do { sig_ty <- tcHsSigType (ForSigCtxt nm) hs_ty
        ; (norm_co, norm_sig_ty, gres) <- normaliseFfiType sig_ty
        ; let
            -- Drop the foralls before inspecting the
index 5ccca77..aea344f 100644 (file)
@@ -5,7 +5,7 @@
 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
 -}
 
-{-# LANGUAGE CPP, TupleSections, MultiWayIf #-}
+{-# LANGUAGE CPP, TupleSections, MultiWayIf, RankNTypes #-}
 
 module TcHsType (
         -- Type signatures
@@ -53,7 +53,7 @@ import TcMType
 import TcValidity
 import TcUnify
 import TcIface
-import TcSimplify ( solveEqualities )
+import TcSimplify ( solveEqualities, solveSomeEqualities )
 import TcType
 import TcHsSyn( zonkSigType )
 import Inst   ( tcInstBinders, tcInstBindersX, tcInstBinderX )
@@ -190,8 +190,7 @@ tcClassSigType :: [Located Name] -> LHsSigType Name -> TcM Type
 -- the recursive class declaration "knot"
 tcClassSigType names sig_ty
   = addSigCtxt (funsSigCtxt names) (hsSigType sig_ty) $
-    do { ty <- tc_hs_sig_type sig_ty liftedTypeKind
-       ; kindGeneralizeType ty }
+    tc_hs_sig_type_and_gen sig_ty liftedTypeKind
 
 tcHsSigType :: UserTypeCtxt -> LHsSigType Name -> TcM Type
 -- Does validity checking
@@ -204,22 +203,37 @@ tcHsSigType ctxt sig_ty
               -- The kind is checked by checkValidType, and isn't necessarily
               -- of kind * in a Template Haskell quote eg [t| Maybe |]
 
-       ; ty <- tc_hs_sig_type sig_ty kind
-
           -- Generalise here: see Note [Kind generalisation]
-       ; do_kind_gen <- decideKindGeneralisationPlan ty
+       ; do_kind_gen <- decideKindGeneralisationPlan sig_ty
        ; ty <- if do_kind_gen
-               then kindGeneralizeType ty
-               else zonkTcType ty
+               then tc_hs_sig_type_and_gen sig_ty kind
+               else tc_hs_sig_type         sig_ty kind >>= zonkTcType
 
        ; checkValidType ctxt ty
        ; return ty }
 
+-- kind-checks/desugars an 'LHsSigType' and then kind-generalizes.
+-- This will never emit constraints, as it uses solveEqualities interally.
+-- No validity checking, but it does zonk en route to generalization
+tc_hs_sig_type_and_gen :: LHsSigType Name -> Kind -> TcM Type
+tc_hs_sig_type_and_gen sig_ty kind
+  = do { ty <- tc_hs_sig_type_x solveEqualities sig_ty kind
+       ; kindGeneralizeType ty }
+
 tc_hs_sig_type :: LHsSigType Name -> Kind -> TcM Type
--- Does not do validity checking or zonking
-tc_hs_sig_type (HsIB { hsib_body = hs_ty
-                     , hsib_vars = sig_vars }) kind
-  = do { (tkvs, ty) <- solveEqualities $
+-- May emit constraints; uses solveSomeEqualities internally.
+-- No zonking or validity checking
+tc_hs_sig_type = tc_hs_sig_type_x solveSomeEqualities
+
+-- Version of tc_hs_sig_type parameterized over how it should solve
+-- equalities
+tc_hs_sig_type_x :: (forall a. TcM a -> TcM a)  -- solveSomeEqualities
+                                                -- or solveEqualities
+                 -> LHsSigType Name -> Kind
+                 -> TcM Type
+tc_hs_sig_type_x solve (HsIB { hsib_body = hs_ty
+                             , hsib_vars = sig_vars }) kind
+  = do { (tkvs, ty) <- solve $
                        tcImplicitTKBndrsType sig_vars $
                        tc_lhs_type typeLevelMode hs_ty kind
        ; return (mkSpecForAllTys tkvs ty) }
@@ -237,8 +251,7 @@ tcHsDeriv hs_ty
                     -- can be no covars in an outer scope
        ; ty <- checkNoErrs $
                  -- avoid redundant error report with "illegal deriving", below
-               tc_hs_sig_type hs_ty cls_kind
-       ; ty <- kindGeneralizeType ty  -- also zonks
+               tc_hs_sig_type_and_gen hs_ty cls_kind
        ; cls_kind <- zonkTcType cls_kind
        ; let (tvs, pred) = splitForAllTys ty
        ; let (args, _) = splitFunTys cls_kind
@@ -252,8 +265,7 @@ tcHsClsInstType :: UserTypeCtxt    -- InstDeclCtxt or SpecInstCtxt
 -- Like tcHsSigType, but for a class instance declaration
 tcHsClsInstType user_ctxt hs_inst_ty
   = setSrcSpan (getLoc (hsSigType hs_inst_ty)) $
-    do { inst_ty <- tc_hs_sig_type hs_inst_ty constraintKind
-       ; inst_ty <- kindGeneralizeType inst_ty
+    do { inst_ty <- tc_hs_sig_type_and_gen hs_inst_ty constraintKind
        ; checkValidInstance user_ctxt hs_inst_ty inst_ty }
 
 -- Used for 'VECTORISE [SCALAR] instance' declarations
@@ -276,7 +288,9 @@ tcHsVectInst ty
 tcHsTypeApp :: LHsWcType Name -> Kind -> TcM Type
 tcHsTypeApp wc_ty kind
   | HsWC { hswc_wcs = sig_wcs, hswc_body = hs_ty } <- wc_ty
-  = do { ty <- solveEqualities $
+    -- use solveSomeEqualities b/c we are in an expression
+    -- See Note [solveEqualities vs solveSomeEqualities] in TcSimplify
+  = do { ty <- solveSomeEqualities $
                tcWildCardBindersX newWildTyVar sig_wcs $ \ _ ->
                tcCheckLHsType hs_ty kind
        ; ty <- zonkTcType ty
@@ -290,8 +304,8 @@ tcHsTypeApp wc_ty kind
 ************************************************************************
 *                                                                      *
             The main kind checker: no validity checks here
-%*                                                                      *
-%************************************************************************
+*                                                                      *
+************************************************************************
 
         First a couple of simple wrappers for kcHsType
 -}
@@ -320,18 +334,14 @@ tcLHsType ty = addTypeCtxt ty (tc_infer_lhs_type typeLevelMode ty)
 
 ---------------------------
 -- | Should we generalise the kind of this type signature?
--- We *should* generalise if the type mentions no scoped type variables
+-- We *should* generalise if the type is closed
 -- or if NoMonoLocalBinds is set. Otherwise, nope.
-decideKindGeneralisationPlan :: Type -> TcM Bool
-decideKindGeneralisationPlan ty
+decideKindGeneralisationPlan :: LHsSigType Name -> TcM Bool
+decideKindGeneralisationPlan sig_ty@(HsIB { hsib_closed = closed })
   = do { mono_locals <- xoptM LangExt.MonoLocalBinds
-       ; in_scope <- getInLocalScope
-       ; let fvs        = tyCoVarsOfTypeList ty
-             should_gen = not mono_locals || all (not . in_scope . getName) fvs
+       ; let should_gen = not mono_locals || closed
        ; traceTc "decideKindGeneralisationPlan"
-           (vcat [ text "type:" <+> ppr ty
-                 , text "ftvs:" <+> ppr fvs
-                 , text "should gen?" <+> ppr should_gen ])
+           (ppr sig_ty $$ text "should gen?" <+> ppr should_gen)
        ; return should_gen }
 
 {-
@@ -1771,13 +1781,16 @@ the term:
   * We instantiate the explicit and implicit foralls with SigTvs
   * We instantiate the wildcards with meta tyvars
 
-We /do/ call solveEqualities, and then zonk to propage the result of
-solveEqualities, mainly so that functions like matchExpectedFunTys will
+We /do/ call solveSomeEqualities, and then zonk to propagate the result of
+solveSomeEqualities, mainly so that functions like matchExpectedFunTys will
 be able to decompose the type, and hence higher-rank signatures will
 work. Ugh!  For example
    f :: (forall a. a->a) -> _
    f x = (x True, x 'c')
 
+Because we are not generalizing, etc., solveSomeEqualities is appropriate.
+See also Note [solveEqualities vs solveSomeEqualities] in TcSimplify.
+
 -}
 
 tcHsPartialSigType
@@ -1795,7 +1808,7 @@ tcHsPartialSigType ctxt sig_ty
   = addSigCtxt ctxt hs_ty $
     do { (implicit_tvs, (wcs, wcx, explicit_tvs, theta, tau))
             <- -- See Note [Solving equalities in partial type signatures]
-               solveEqualities $
+               solveSomeEqualities $
                tcWildCardBindersX newWildTyVar sig_wcs        $ \ wcs ->
                tcImplicitTKBndrsX new_implicit_tv implicit_hs_tvs $
                tcExplicitTKBndrsX newSigTyVar explicit_hs_tvs $ \ explicit_tvs ->
@@ -1857,7 +1870,7 @@ tcHsPatSigType ctxt sig_ty
   = addSigCtxt ctxt hs_ty $
     do { (implicit_tvs, (wcs, sig_ty))
             <- -- See Note [Solving equalities in partial type signatures]
-               solveEqualities $
+               solveSomeEqualities $
                tcWildCardBindersX newWildTyVar    sig_wcs  $ \ wcs ->
                tcImplicitTKBndrsX new_implicit_tv sig_vars $
                do { sig_ty <- tcHsOpenType hs_ty
index d3fd768..e2b9fe6 100644 (file)
@@ -6,7 +6,7 @@ module TcSimplify(
        simplifyAmbiguityCheck,
        simplifyDefault,
        simplifyTop, simplifyTopImplic, captureTopConstraints,
-       simplifyInteractive, solveEqualities,
+       simplifyInteractive, solveSomeEqualities, solveEqualities,
        simplifyWantedsTcM,
        tcCheckSatisfiability,
 
@@ -128,8 +128,68 @@ simplifyTop wanteds
 
        ; return (evBindMapBinds binds1 `unionBags` binds2) }
 
+{- Note [solveEqualities vs solveSomeEqualities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When kind-checking a type, GHC might generate equality constraints. (We know
+it will generate only *equalities*, not e.g. class constraints, because types
+don't contain class methods.) What should we do with these constraints?
+Before we can effectively zonk, generalize, or validity-check a type, we need
+to solve these equalities. The functions solveEqualities and solveSomeEqualities
+do precisely this.
+
+solveEqualities solves *all* equality constraints generated by the thing_inside.
+If any constraints are unable to be solved, fail. This is appropriate for a top-
+level type where we absolutely must, say, generalize right away. For example,
+in
+
+    data G (a :: k) where
+      MkG :: G Maybe
+
+The type G Maybe will make equality constraints that must be handled pronto.
+
+solveSomeEqualities, on the other hand, does the best it can, re-emitting those
+constraints it can't solve. This is appropriate when, for example, a type
+appears in the middle of an expression (either a type annotation or a visible
+type application) and there may be givens that have a bearing on whether or
+not a type-level equality is soluble. The use of solveEqualities in an type
+annotation is what gave rise to #13337.
+
+Why have solveSomeEqualities at all, instead of just letting all equality
+constraints go where all the other constraints do? Because we want to nail what
+equalities we can before doing validity checking. Otherwise, the validity checker
+may see casts and other nonsense in what should be a simple type.
+
+How to choose between these?
+
+Use solveEqualities when any of the following apply:
+  * you are about to kind-generalize
+  * you are about to call zonkTcTypeToType
+  * you are in a top-level context, not inside of any expression
+
+Use solveSomeEqualities when:
+  * none of the above applies
+-}
+
+-- | Type-check a thing that emits only equality constraints, then
+-- solve as many constraints as possible. Re-emits any unsolved constraints.
+-- Never fails. This is useful when you're in a context where emitting
+-- constraints is a good idea (e.g., in a expression type signature) but
+-- you also want to use a function from TcValidity. TcValidity wants the
+-- type to be as well-defined as possible. So this does what it can.
+-- See also Note [solveEqualities vs solveSomeEqualities]
+solveSomeEqualities :: TcM a -> TcM a
+solveSomeEqualities thing_inside
+  = do { (result, wanted) <- captureConstraints thing_inside
+       ; traceTc "solveSomeEqualities {" $ text "wanted = " <+> ppr wanted
+       ; final_wc <- runTcSEqualities $ simpl_top wanted
+       ; traceTc "End solveESomequalities }" empty
+
+       ; emitConstraints final_wc
+       ; return result }
+
 -- | Type-check a thing that emits only equality constraints, then
 -- solve those constraints. Fails outright if there is trouble.
+-- See also Note [solveEqualities vs solveSomeEqualities]
 solveEqualities :: TcM a -> TcM a
 solveEqualities thing_inside
   = checkNoErrs $  -- See Note [Fail fast on kind errors]
index 6f30537..2a2b553 100644 (file)
@@ -1066,7 +1066,8 @@ tcDefaultAssocDecl fam_tc [L loc (TyFamEqn { tfe_tycon = L _ tc_name
 
        -- Typecheck RHS
        ; let pats = HsIB { hsib_vars = imp_vars ++ map hsLTyVarName exp_vars
-                         , hsib_body = map hsLTyVarBndrToType exp_vars }
+                         , hsib_body = map hsLTyVarBndrToType exp_vars
+                         , hsib_closed = False } -- this field is ignored, anyway
           -- NB: Use tcFamTyPats, not tcTyClTyVars. The latter expects to get
           -- the LHsQTyVars used for declaring a tycon, but the names here
           -- are different.
index 9f6b869..9f9cf65 100644 (file)
@@ -92,7 +92,8 @@
                       (HsTyVar 
                        (NotPromoted) 
                        ({ DumpParsedAst.hs:8:15-16 }
-                        (Unqual {OccName: as}))))))]))))]) 
+                        (Unqual {OccName: as}))))))]))))] 
+             (PlaceHolder)) 
             (Prefix) 
             ({ DumpParsedAst.hs:8:21-36 }
              (HsAppsTy 
                (HsExplicitListTy 
                 (Promoted) 
                 (PlaceHolder) 
-                []))]) 
+                []))] 
+             (PlaceHolder)) 
             (Prefix) 
             ({ DumpParsedAst.hs:9:21-24 }
              (HsAppsTy 
index 437390c..d0b456a 100644 (file)
                   ({ DumpRenamedAst.hs:8:15-16 }
                    (HsTyVar 
                     (NotPromoted) 
-                    ({ DumpRenamedAst.hs:8:15-16 }{Name: as{tv}})))))))]) 
+                    ({ DumpRenamedAst.hs:8:15-16 }{Name: as{tv}})))))))] 
+             (True)) 
             (Prefix) 
             ({ DumpRenamedAst.hs:8:21-36 }
              (HsAppTy 
                (HsExplicitListTy 
                 (Promoted) 
                 (PlaceHolder) 
-                []))]) 
+                []))] 
+             (True)) 
             (Prefix) 
             ({ DumpRenamedAst.hs:9:21-24 }
              (HsTyVar 
index 7bfe118..129cd03 100644 (file)
@@ -1,5 +1,12 @@
 
 T11976.hs:7:20: error:
+    • Illegal polymorphic type: Lens w0 w1
+      GHC doesn't yet support impredicative polymorphism
+    • In an expression type signature: Lens _ _ _
+      In the expression: undefined :: Lens _ _ _
+      In an equation for ‘foo’: foo = undefined :: Lens _ _ _
+
+T11976.hs:7:20: error:
     • Expecting one fewer arguments to ‘Lens w0 w1’
       Expected kind ‘k0 -> *’, but ‘Lens w0 w1’ has kind ‘*’
     • In the type ‘Lens _ _ _’
index 4287110..7f1d713 100644 (file)
@@ -1,8 +1,15 @@
 
+T12634.hs:14:37: error:
+    • Found type wildcard ‘_’ standing for ‘() :: Constraint’
+      To use the inferred type, enable PartialTypeSignatures
+    • In the type signature:
+        bench_twacePow :: forall t m m' r.
+                          _ => t m' r -> Bench '(t, m, m', r)
+
 T12634.hs:14:58: error:
     • Expected a type, but
       ‘'(t, m, m', r)’ has kind
-      ‘(k1 -> k2 -> *, k0, k1, k2)’
+      ‘(* -> * -> *, *, *, *)’
     • In the first argument of ‘Bench’, namely ‘'(t, m, m', r)’
       In the type ‘t m' r -> Bench '(t, m, m', r)’
       In the type signature:
diff --git a/testsuite/tests/typecheck/should_compile/T13337.hs b/testsuite/tests/typecheck/should_compile/T13337.hs
new file mode 100644 (file)
index 0000000..39808b4
--- /dev/null
@@ -0,0 +1,16 @@
+{-# LANGUAGE TypeInType, ScopedTypeVariables, TypeOperators, GADTs #-}
+{-# OPTIONS_GHC -Wno-overlapping-patterns #-}  -- don't want erroneous warning in test output
+                                               -- if removing this doesn't change output, then
+                                               -- remove it!
+
+module T13337 where
+
+import Data.Typeable
+import Data.Kind
+
+f :: forall k (a :: k). (Typeable k, Typeable a) => Proxy a -> Proxy Int
+f p = case eqT :: Maybe (k :~: Type) of
+  Nothing -> Proxy
+  Just Refl -> case eqT :: Maybe (a :~: Int) of
+    Nothing -> Proxy
+    Just Refl -> p
index 29b28df..d2dd684 100644 (file)
@@ -544,3 +544,4 @@ test('T12923', normal, compile, [''])
 test('T12924', normal, compile, [''])
 test('T12926', normal, compile, [''])
 test('T13381', normal, compile_fail, [''])
+test('T13337', normal, compile, [''])
index 9acb289..12a6cc9 160000 (submodule)
@@ -1 +1 @@
-Subproject commit 9acb2890cdb4369f3bb7fda899ff4d3526040e7d
+Subproject commit 12a6cc9a98b79a4851fbe40a02c56652338d1c3e