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

Commits:

6 changed files:

Changes:

  • compiler/GHC/Tc/Solver/Equality.hs
    ... ... @@ -197,12 +197,8 @@ zonkEqTypes ev eq_rel ty1 ty2
    197 197 
             then tycon tc1 tys1 tys2
    198 198 
             else bale_out ty1 ty2
    199 199
    200 
    -    go ty1 ty2
    201 
    -      | Just (ty1a, ty1b) <- tcSplitAppTyNoView_maybe ty1
    202 
    -      , Just (ty2a, ty2b) <- tcSplitAppTyNoView_maybe ty2
    203 
    -      = do { res_a <- go ty1a ty2a
    204 
    -           ; res_b <- go ty1b ty2b
    205 
    -           ; return $ combine_rev mkAppTy res_b res_a }
    200 
    +    -- If you are temppted to add a case for AppTy/AppTy, be careful
    201 
    +    -- See Note [zonkEqTypes and the PKTI]
    206 202
    207 203 
         go ty1@(LitTy lit1) (LitTy lit2)
    208 204 
           | lit1 == lit2
    ... ... @@ -278,6 +274,32 @@ zonkEqTypes ev eq_rel ty1 ty2
    278 274 
         combine_rev f (Right tys) (Right ty) = Right (f ty tys)
    279 275
    280 276
    277 
    +{- Note [zonkEqTypes and the PKTI]
    278 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    279 
    +Because `zonkEqTypes` does /partial/ zonking, we need to be very careful
    280 
    +to maintain the Purely Kinded Type Invariant: see GHC.Tc.Gen/HsType
    281 
    +HsNote [The Purely Kinded Type Invariant (PKTI)].
    282 
    +
    283 
    +In #26256 we try to solve this equality constraint:
    284 
    +   Int :-> Maybe Char ~# k0 Int (m0 Char)
    285 
    +where m0 and k0 are unification variables, and
    286 
    +   m0 :: Type -> Type
    287 
    +It happens that m0 was already unified
    288 
    +   m0 := (w0 :: kappa)
    289 
    +where kappa is another unification variable that is also already unified:
    290 
    +   kappa := Type->Type.
    291 
    +So the original type satisifed the PKTI, but a partially-zonked form
    292 
    +   k0 Int (w0 Char)
    293 
    +does not!! (This a bit reminiscent of Note [mkAppTyM].)
    294 
    +
    295 
    +The solution I have adopted is simply to make `zonkEqTypes` bale out on `AppTy`.
    296 
    +After all, it's only supposed to be a quick hack to see if two types are already
    297 
    +equal; if we bale out we'll just get into the "proper" canonicaliser.
    298 
    +
    299 
    +The only tricky thing about this approach is that it relies on /omitting/
    300 
    +code -- for the AppTy/AppTy case!  Hence this Note
    301 
    +-}
    302 
    +
    281 303 
     {- *********************************************************************
    282 304 
     *                                                                      *
    283 305 
     *           canonicaliseEquality

  • testsuite/tests/partial-sigs/should_compile/T26256.hs
    1 
    +{-# LANGUAGE GHC2021 #-}
    2 
    +{-# LANGUAGE TypeFamilies #-}
    3 
    +{-# LANGUAGE PartialTypeSignatures #-}
    4 
    +
    5 
    +module M (go) where
    6 
    +
    7 
    +import Data.Kind
    8 
    +
    9 
    +type Apply :: (Type -> Type) -> Type
    10 
    +data Apply m
    11 
    +
    12 
    +type (:->) :: Type -> Type -> Type
    13 
    +type family (:->) where (:->) = (->)
    14 
    +
    15 
    +f :: forall (k :: Type -> Type -> Type) (m :: Type -> Type).
    16 
    +     k Int (m Char) -> k Bool (Apply m)
    17 
    +f = f
    18 
    +
    19 
    +x :: Int :-> Maybe Char
    20 
    +x = x
    21 
    +
    22 
    +go :: Bool -> _ _
    23 
    +go = f x

  • testsuite/tests/partial-sigs/should_compile/T26256.stderr
    1 
    +T26256.hs:22:15: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
    2 
    +    • Found type wildcard ‘_’ standing for ‘Apply :: (* -> *) -> *’
    3 
    +    • In the type signature: go :: Bool -> _ _
    4 
    +
    5 
    +T26256.hs:22:17: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
    6 
    +    • Found type wildcard ‘_’ standing for ‘Maybe :: * -> *’
    7 
    +    • In the first argument of ‘_’, namely ‘_’
    8 
    +      In the type signature: go :: Bool -> _ _

  • testsuite/tests/partial-sigs/should_compile/all.T
    ... ... @@ -108,3 +108,4 @@ test('T21667', normal, compile, [''])
    108 108 
     test('T22065', normal, compile, [''])
    109 109 
     test('T16152', normal, compile, [''])
    110 110 
     test('T20076', expect_broken(20076), compile, [''])
    111 
    +test('T26256', normal, compile, [''])

  • testsuite/tests/typecheck/should_compile/T26256a.hs
    1 
    +{-# LANGUAGE GHC2021 #-}
    2 
    +{-# LANGUAGE TypeFamilies #-}
    3 
    +
    4 
    +module T26256 (go) where
    5 
    +
    6 
    +import Data.Kind
    7 
    +
    8 
    +class Cat k where (<<<) :: k a b -> k x a -> k x b
    9 
    +instance Cat (->) where (<<<) = (.)
    10 
    +class Pro k p where pro :: k a b s t -> p a b -> p s t
    11 
    +data Hiding o a b s t = forall e. Hiding (s -> o e a)
    12 
    +newtype Apply e a = Apply (e a)
    13 
    +
    14 
    +type (:->) :: Type -> Type -> Type
    15 
    +type family (:->) where
    16 
    +  (:->) = (->)
    17 
    +
    18 
    +go :: (Pro (Hiding Apply) p) => (s :-> e a) -> p a b -> p s t
    19 
    +go sea = pro (Hiding (Apply <<< sea))

  • testsuite/tests/typecheck/should_compile/all.T
    ... ... @@ -940,3 +940,4 @@ test('T26020', normal, compile, [''])
    940 940 
     test('T26020a', [extra_files(['T26020a_help.hs'])], multimod_compile, ['T26020a', '-v0'])
    941 941 
     test('T25992', normal, compile, [''])
    942 942 
     test('T14010', normal, compile, [''])
    943 
    +test('T26256a', normal, compile, [''])

    • —
    View it on GitLab.
    You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications · Help