[Git][ghc/ghc][wip/T24810] Wibbles

Simon Peyton Jones (@simonpj) gitlab at gitlab.haskell.org
Fri May 17 06:50:39 UTC 2024



Simon Peyton Jones pushed to branch wip/T24810 at Glasgow Haskell Compiler / GHC


Commits:
d9babc57 by Simon Peyton Jones at 2024-05-16T23:35:02+01:00
Wibbles

- - - - -


5 changed files:

- compiler/GHC/Tc/Utils/Instantiate.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- + testsuite/tests/typecheck/should_compile/T24810.hs
- testsuite/tests/typecheck/should_compile/all.T


Changes:

=====================================
compiler/GHC/Tc/Utils/Instantiate.hs
=====================================
@@ -205,8 +205,7 @@ topSkolemise skolem_info ty
 skolemiseRequired :: SkolemInfo -> VisArity -> TcSigmaType
                   -> TcM (VisArity, HsWrapper, [Name], [ForAllTyBinder], [EvVar], TcSigmaType)
 -- Skolemise up to N required (visible) binders, plus any invisible ones
--- "in the way". Stop as soon as you have found the n'th, so there might still
--- be some invisible foralls/qual-tys in the returned type
+-- "in the way", and any trailing invisible ones.
 -- Return the depleted arity
 skolemiseRequired skolem_info n_req sigma
   = go n_req init_subst idHsWrapper [] [] [] sigma
@@ -215,8 +214,7 @@ skolemiseRequired skolem_info n_req sigma
 
     -- Why recursive?  See Note [Skolemisation]
     go n_req subst wrap acc_nms acc_bndrs ev_vars ty
-      | n_req > 0
-      , (n_req', bndrs, inner_ty) <- tcSplitForAllTyVarsReqTVBindersN n_req ty
+      | (n_req', bndrs, inner_ty) <- tcSplitForAllTyVarsReqTVBindersN n_req ty
       , not (null bndrs)
       = do { (subst', bndrs1) <- tcInstSkolTyVarBndrsX skolem_info subst bndrs
            ; let tvs1 = binderVars bndrs1
@@ -227,8 +225,7 @@ skolemiseRequired skolem_info n_req sigma
                 ev_vars
                 inner_ty }
 
-      | n_req > 0
-      , (theta, inner_ty) <- tcSplitPhiTy ty
+      | (theta, inner_ty) <- tcSplitPhiTy ty
       , not (null theta)
       = do { ev_vars1 <- newEvVars (substTheta subst theta)
            ; go n_req subst


=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -1412,15 +1412,15 @@ tcSplitSomeForAllTyVars argf_pred ty
 
 tcSplitForAllTyVarsReqTVBindersN :: Arity -> Type -> (Arity, [ForAllTyBinder], Type)
 -- Split off at most N /required/ (aka visible) binders, plus any invisible ones in the way
+-- and any trailing invisibl ones
 tcSplitForAllTyVarsReqTVBindersN n_req ty
   = split n_req ty ty []
   where
-    split 0 orig_ty _ty bs                              = (0, reverse bs, orig_ty)
     split n_req _orig_ty (ForAllTy b@(Bndr _ argf) ty) bs
-      | isVisibleForAllTyFlag argf                      = split (n_req - 1) ty ty (b:bs)
+      | isVisibleForAllTyFlag argf, n_req > 0           = split (n_req - 1) ty ty (b:bs)
       | otherwise                                       = split n_req       ty ty (b:bs)
     split n_req orig_ty ty bs | Just ty' <- coreView ty = split n_req orig_ty ty' bs
-    split _n_req orig_ty _ty bs                         = (n_req, reverse bs, orig_ty)
+    split n_req orig_ty _ty bs                          = (n_req, reverse bs, orig_ty)
 
 -- | Like 'tcSplitForAllTyVars', but only splits 'ForAllTy's with 'Required' type
 -- variable binders. All split tyvars are annotated with '()'.


=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -786,38 +786,8 @@ matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside
     --     i.e. length (filterOut isExpForAllPatTyInvis rev_pat_tys)
 
     -- Do shallow skolemisation if there are top-level invisible quantifiers
-    check n_so_far rev_pat_tys ty
-      | isSigmaTy ty  -- Type has invisible quantifiers
-      = do { (wrap_gen, (wrap_res, result))
-                 <- tcSkolemiseGeneral Shallow ctx top_ty ty $ \tv_bndrs ty' ->
-                    let rev_pat_tys' = reverse (map (mkInvisExpPatType . snd) tv_bndrs)
-                                       ++ rev_pat_tys
-                    in check n_so_far rev_pat_tys' ty'
-           ; return (wrap_gen <.> wrap_res, result) }
-
-    ----------------------------
-    -- Base case: (n_so_far == arity): no more args
-    --    rho_ty has no top-level quantifiers
-    --    If there is deep subsumption, do deep skolemisation
-    check n_so_far rev_pat_tys rho_ty
-      | n_so_far == arity
-      = do { let pat_tys = reverse rev_pat_tys
-           ; ds_flag <- getDeepSubsumptionFlag
-           ; case ds_flag of
-               Shallow -> do { res <- thing_inside pat_tys (mkCheckExpType rho_ty)
-                             ; return (idHsWrapper, res) }
-               Deep    -> tcSkolemiseGeneral Deep ctx top_ty rho_ty $ \_ rho_ty ->
-                          -- "_" drop the /deeply/-skolemise binders
-                          -- They do not line up with binders in the Match
-                          thing_inside pat_tys (mkCheckExpType rho_ty) }
-
-    -- NOW do coreView.  We didn't do it before, so that we do not unnecessarily
-    -- unwrap a synonym in the returned rho_ty
-    check n_so_far rev_pat_tys ty
-      | Just ty' <- coreView ty = check n_so_far rev_pat_tys ty'
-
     ----------------------------
-    -- Visible forall
+    -- Skolemise quantifiers
     --
     -- Decompose /visible/ (forall a -> blah), to give an ExpForAllPat
     -- NB: invisible binders are handled by tcSplitSigmaTy/tcTopSkolemise above
@@ -825,9 +795,9 @@ matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside
     --     to syntactically visible patterns in the source program
     -- See Note [Visible type application and abstraction] in GHC.Tc.Gen.App
     check n_so_far rev_pat_tys ty
-      | isForAllTy ty  -- isSigmaTy case above has dealt with /invisible/ quantifiers,
-                       -- so this one must be /visible/ (= Required)
-      , let n_req = arity - n_so_far  -- Must be n_req > 0
+      | let n_req = arity - n_so_far
+      , isSigmaTy ty                     -- Invisible quantifier at the top
+        || (n_req > 0 && isForAllTy ty)  -- Visible quantifier at top, and we need it
       = do { rec { (n_req', wrap_gen, tv_nms, bndrs, given, inner_ty) <- skolemiseRequired skol_info n_req ty
                  ; let sig_skol = SigSkol ctx top_ty (tv_nms `zip` skol_tvs)
                        skol_tvs = binderVars bndrs
@@ -840,9 +810,30 @@ matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside
                      check (arity - n_req')
                            (reverse pat_tys ++ rev_pat_tys)
                            inner_ty
-           ; assertPpr (n_req' < n_req) (ppr ty) $  -- Some progress
+           ; assertPpr (not (null bndrs && null given)) (ppr ty) $  -- Some progress
              return (wrap_gen <.> mkWpLet ev_binds <.> wrap_res, result) }
 
+    ----------------------------
+    -- Base case: (n_so_far == arity): no more args
+    --    rho_ty has no top-level invisible quantifiers
+    --    If there is deep subsumption, do deep skolemisation
+    check n_so_far rev_pat_tys rho_ty
+      | n_so_far == arity
+      = do { let pat_tys = reverse rev_pat_tys
+           ; ds_flag <- getDeepSubsumptionFlag
+           ; case ds_flag of
+               Shallow -> do { res <- thing_inside pat_tys (mkCheckExpType rho_ty)
+                             ; return (idHsWrapper, res) }
+               Deep    -> tcSkolemiseGeneral Deep ctx top_ty rho_ty $ \_ rho_ty ->
+                          -- "_" drop the /deeply/-skolemise binders
+                          -- They do not line up with binders in the Match
+                          thing_inside pat_tys (mkCheckExpType rho_ty) }
+
+    -- NOW do coreView.  We didn't do it before, so that we do not unnecessarily
+    -- unwrap a synonym in the returned rho_ty
+    check n_so_far rev_pat_tys ty
+      | Just ty' <- coreView ty = check n_so_far rev_pat_tys ty'
+
     ----------------------------
     -- Function types
     check n_so_far rev_pat_tys (FunTy { ft_af = af, ft_mult = mult


=====================================
testsuite/tests/typecheck/should_compile/T24810.hs
=====================================
@@ -0,0 +1,15 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T24810 where
+
+import GHC.TypeLits
+
+showKnownChar :: forall c -> KnownChar c => IO ()
+showKnownChar c = print (charSing @c)
+
+withKnownChar_rta :: SChar c -> (forall c' -> c ~ c' => KnownChar c => r) -> r
+withKnownChar_rta (SChar @c) r = r c
+
+-- no type signature
+example = withKnownChar_rta (SChar @'a') (\c -> showKnownChar c)


=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -916,3 +916,4 @@ test('T24470b', normal, compile, [''])
 test('T24566', [], makefile_test, [])
 test('T23764', normal, compile, [''])
 test('T23739a', normal, compile, [''])
+test('T24810', normal, compile, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d9babc5722116535352294c2e3b6941808b96129

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d9babc5722116535352294c2e3b6941808b96129
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20240517/f6e7ab13/attachment-0001.html>


More information about the ghc-commits mailing list