[Git][ghc/ghc][wip/sand-witch/lazy-skol] Fix assertion error

[Simon Peyton Jones (@simonpj)]

Simon Peyton Jones pushed to branch wip/sand-witch/lazy-skol at Glasgow Haskell Compiler / GHC


Commits:
941e15ed by Simon Peyton Jones at 2024-01-09T10:09:56+00:00
Fix assertion error

- - - - -


2 changed files:

- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Tc/Utils/TcType.hs


Changes:

=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -736,22 +736,6 @@ mkInvisFunTys args res
   where
     af = invisArg (typeTypeOrConstraint res)
 
-tcMkVisFunTy :: Mult -> Type -> Type -> Type
--- Always TypeLike, user-specified multiplicity.
--- Does not have the assert-checking in mkFunTy: used by the typechecker
--- to avoid looking at the result kind, which may not be zonked
-tcMkVisFunTy mult arg res
-  = FunTy { ft_af = visArgTypeLike, ft_mult = mult
-          , ft_arg = arg, ft_res = res }
-
-tcMkInvisFunTy :: TypeOrConstraint -> Type -> Type -> Type
--- Always TypeLike, invisible argument
--- Does not have the assert-checking in mkFunTy: used by the typechecker
--- to avoid looking at the result kind, which may not be zonked
-tcMkInvisFunTy res_torc arg res
-  = FunTy { ft_af = invisArg res_torc, ft_mult = manyDataConTy
-          , ft_arg = arg, ft_res = res }
-
 mkVisFunTy :: HasDebugCallStack => Mult -> Type -> Type -> Type
 -- Always TypeLike, user-specified multiplicity.
 mkVisFunTy = mkFunTy visArgTypeLike
@@ -777,16 +761,6 @@ mkScaledFunTys :: HasDebugCallStack => [Scaled Type] -> Type -> Type
 mkScaledFunTys tys ty = foldr (mkScaledFunTy af) ty tys
   where
     af = visArg (typeTypeOrConstraint ty)
-
-tcMkScaledFunTys :: [Scaled Type] -> Type -> Type
--- All visible args
--- Result type must be TypeLike
--- No mkFunTy assert checking; result kind may not be zonked
-tcMkScaledFunTys tys ty = foldr tcMkScaledFunTy ty tys
-
-tcMkScaledFunTy :: Scaled Type -> Type -> Type
-tcMkScaledFunTy (Scaled mult arg) res = tcMkVisFunTy mult arg res
-
 ---------------
 -- | Like 'mkTyCoForAllTy', but does not check the occurrence of the binder
 -- See Note [Unused coercion variable in ForAllTy]
@@ -811,7 +785,7 @@ mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
 mkInvisForAllTys :: [InvisTVBinder] -> Type -> Type
 mkInvisForAllTys tyvars = mkForAllTys (tyVarSpecToBinders tyvars)
 
-mkPiTy :: PiTyBinder -> Type -> Type
+mkPiTy :: HasDebugCallStack => PiTyBinder -> Type -> Type
 mkPiTy (Anon ty1 af) ty2  = mkScaledFunTy af ty1 ty2
 mkPiTy (Named bndr) ty    = mkForAllTy bndr ty
 
@@ -826,6 +800,32 @@ mkPiTys tbs ty = foldr mkPiTy ty tbs
 mkNakedTyConTy :: TyCon -> Type
 mkNakedTyConTy tycon = TyConApp tycon []
 
+tcMkVisFunTy :: Mult -> Type -> Type -> Type
+-- Always TypeLike, user-specified multiplicity.
+-- Does not have the assert-checking in mkFunTy: used by the typechecker
+-- to avoid looking at the result kind, which may not be zonked
+tcMkVisFunTy mult arg res
+  = FunTy { ft_af = visArgTypeLike, ft_mult = mult
+          , ft_arg = arg, ft_res = res }
+
+tcMkInvisFunTy :: TypeOrConstraint -> Type -> Type -> Type
+-- Always TypeLike, invisible argument
+-- Does not have the assert-checking in mkFunTy: used by the typechecker
+-- to avoid looking at the result kind, which may not be zonked
+tcMkInvisFunTy res_torc arg res
+  = FunTy { ft_af = invisArg res_torc, ft_mult = manyDataConTy
+          , ft_arg = arg, ft_res = res }
+
+tcMkScaledFunTys :: [Scaled Type] -> Type -> Type
+-- All visible args
+-- Result type must be TypeLike
+-- No mkFunTy assert checking; result kind may not be zonked
+tcMkScaledFunTys tys ty = foldr tcMkScaledFunTy ty tys
+
+tcMkScaledFunTy :: Scaled Type -> Type -> Type
+tcMkScaledFunTy (Scaled mult arg) res = tcMkVisFunTy mult arg res
+
+
 {-
 %************************************************************************
 %*                                                                      *


=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -478,14 +478,14 @@ isExpFunPatTy ExpForAllPatTy{} = False
 reconstructCheckType :: [ExpPatType] -> ExpType -> TcType
 -- Precondition: all the arguments are Check{}
 reconstructCheckType pat_tys res_ty
-  = mkPiTys (mapMaybe prepare_arg_ty pat_tys) (checkingExpType res_ty)
+  = foldr go (checkingExpType res_ty) pat_tys
   where
-    prepare_arg_ty :: ExpPatType -> Maybe PiTyBinder
-    prepare_arg_ty (ExpFunPatTy (Scaled u v))
-      = Just (Anon (Scaled u (checkingExpType v)) visArgTypeLike)
-    prepare_arg_ty (ExpForAllPatTy bndr)
-      | isVisibleForAllTyBinder bndr = Just (Named bndr)
-      | otherwise                    = Nothing
+    go :: ExpPatType -> TcType -> TcType
+    go (ExpFunPatTy (Scaled u v)) res_ty
+      = tcMkVisFunTy u (checkingExpType v) res_ty
+    go (ExpForAllPatTy bndr) res_ty
+      | isVisibleForAllTyBinder bndr = mkForAllTy bndr res_ty
+      | otherwise                    = res_ty
 
 instance Outputable ExpPatType where
   ppr (ExpFunPatTy t) = ppr t



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/941e15ed779610940a58ab40be6216a7051977b3
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/20240109/90ffdb9a/attachment-0001.html>