Simon Peyton Jones pushed to branch wip/T26746 at Glasgow Haskell Compiler / GHC
Commits:
-
96c19504
by Simon Peyton Jones at 2026-01-12T23:49:44+00:00
3 changed files:
- compiler/GHC/Core/FamInstEnv.hs
- compiler/GHC/Tc/Instance/Family.hs
- compiler/GHC/Tc/Solver/Equality.hs
Changes:
| ... | ... | @@ -1061,10 +1061,10 @@ lookup_fam_inst_env' lookup_mode (FamIE _ ie) fam match_tys |
| 1061 | 1061 | , fi_tys = tpl_tys }) = do
|
| 1062 | 1062 | subst <- tcMatchTys tpl_tys match_tys1
|
| 1063 | 1063 | return (FamInstMatch { fim_instance = item
|
| 1064 | - , fim_tys = substTyVars subst tpl_tvs `chkAppend` match_tys2
|
|
| 1065 | - , fim_cos = assert (all (isJust . lookupCoVar subst) tpl_cvs) $
|
|
| 1066 | - substCoVars subst tpl_cvs
|
|
| 1067 | - })
|
|
| 1064 | + , fim_tys = substTyVars subst tpl_tvs `chkAppend` match_tys2
|
|
| 1065 | + , fim_cos = assert (all (isJust . lookupCoVar subst) tpl_cvs) $
|
|
| 1066 | + substCoVars subst tpl_cvs
|
|
| 1067 | + })
|
|
| 1068 | 1068 | where
|
| 1069 | 1069 | (match_tys1, match_tys2) = split_tys tpl_tys
|
| 1070 | 1070 |
| ... | ... | @@ -451,25 +451,27 @@ tcLookupDataFamInst_maybe fam_inst_envs tc tc_args |
| 451 | 451 | | otherwise
|
| 452 | 452 | = Nothing
|
| 453 | 453 | |
| 454 | --- | 'tcUnwrapNewtype_mabye' gets rid of top-level newtypes,
|
|
| 455 | --- potentially also looking through newtype /instances/
|
|
| 454 | +-- | 'tcUnwrapNewtype_mabye' gets rid of /one layer/ of top-level newtypes
|
|
| 456 | 455 | --
|
| 457 | 456 | -- It is only used by the type inference engine (specifically, when
|
| 458 | 457 | -- solving representational equality), and hence it is careful to unwrap
|
| 459 | 458 | -- only if the relevant data constructor is in scope. That's why
|
| 460 | 459 | -- it gets a GlobalRdrEnv argument.
|
| 461 | 460 | --
|
| 462 | --- It is careful not to unwrap data/newtype instances if it can't
|
|
| 463 | --- unwrap the newtype inside it. Such care is necessary for proper
|
|
| 464 | --- error messages.
|
|
| 461 | +-- It is capable of unwrapping a newtype /instance/. E.g
|
|
| 462 | +-- data D a
|
|
| 463 | +-- newtype instance D Int = MkD Bool
|
|
| 464 | +-- Then `tcUnwrapNewtype_maybe (D Int)` will unwrap to give the `Bool` inside.
|
|
| 465 | +-- However, it is careful not to unwrap data/newtype instances if it can't
|
|
| 466 | +-- unwrap the newtype inside it; that might in the example if `MkD` was
|
|
| 467 | +-- not in scope. Such care is necessary for proper error messages.
|
|
| 465 | 468 | --
|
| 466 | 469 | -- It does not look through type families.
|
| 467 | --- It does not normalise arguments to a tycon.
|
|
| 470 | +-- It does not normalise arguments to the tycon.
|
|
| 468 | 471 | --
|
| 469 | --- If the result is Just ((gres, co), rep_ty), then
|
|
| 472 | +-- If the result is Just (gre, co, rep_ty), then
|
|
| 470 | 473 | -- co : ty ~R rep_ty
|
| 471 | --- gres are the GREs for the data constructors that
|
|
| 472 | --- had to be in scope
|
|
| 474 | +-- gre is the GRE for the data constructor that had to be in scope
|
|
| 473 | 475 | tcUnwrapNewtype_maybe :: FamInstEnvs
|
| 474 | 476 | -> GlobalRdrEnv
|
| 475 | 477 | -> Type
|
| ... | ... | @@ -333,14 +333,6 @@ can_eq_nc rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2 |
| 333 | 333 | | Just ty1' <- coreView ty1 = can_eq_nc rewritten rdr_env envs ev eq_rel ty1' ps_ty1 ty2 ps_ty2
|
| 334 | 334 | | Just ty2' <- coreView ty2 = can_eq_nc rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2' ps_ty2
|
| 335 | 335 | |
| 336 | --- When working with ReprEq, unwrap newtypes.
|
|
| 337 | --- See Note [Eager reflexivity check]
|
|
| 338 | --- See Note [Unwrap newtypes first]
|
|
| 339 | --- This must be above the TyVarTy case, in order to guarantee (TyEq:N)
|
|
| 340 | ---
|
|
| 341 | --- We unwrap *one layer only*; `can_eq_newtype_nc` then loops back to
|
|
| 342 | --- `can_eq_nc`. If there is a recursive newtype, so that we keep
|
|
| 343 | --- unwrapping, the depth limit in `can_eq_newtype_nc` will blow up.
|
|
| 344 | 336 | can_eq_nc _rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _
|
| 345 | 337 | | ReprEq <- eq_rel
|
| 346 | 338 | , TyConApp tc1 tys1 <- ty1
|
| ... | ... | @@ -366,6 +358,14 @@ can_eq_nc _rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _ |
| 366 | 358 | ok _ _ [] = False -- Oversaturated TyCon
|
| 367 | 359 | ok _ _ _ = pprPanic "can_eq_nc:mismatch" (ppr ty1 $$ ppr ty2)
|
| 368 | 360 | |
| 361 | +-- Unwrap newtypes, when in ReprEq only
|
|
| 362 | +-- See Note [Eager reflexivity check]
|
|
| 363 | +-- See Note [Unwrap newtypes first]
|
|
| 364 | +-- This must be above the TyVarTy case, in order to guarantee (TyEq:N)
|
|
| 365 | +--
|
|
| 366 | +-- We unwrap *one layer only*; `can_eq_newtype_nc` then loops back to
|
|
| 367 | +-- `can_eq_nc`. If there is a recursive newtype, so that we keep
|
|
| 368 | +-- unwrapping, the depth limit in `can_eq_newtype_nc` will blow up.
|
|
| 369 | 369 | can_eq_nc _rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
|
| 370 | 370 | | ReprEq <- eq_rel
|
| 371 | 371 | , Just stuff1 <- tcUnwrapNewtype_maybe envs rdr_env ty1
|