[Git][ghc/ghc][wip/cfuneqcan-refactor] 2 commits: Update Note [TyVar/TyVar orientation]

[Richard Eisenberg]

Richard Eisenberg pushed to branch wip/cfuneqcan-refactor at Glasgow Haskell Compiler / GHC


Commits:
05b06a8d by Richard Eisenberg at 2020-11-04T14:41:37-05:00
Update Note [TyVar/TyVar orientation]

- - - - -
9d122639 by Richard Eisenberg at 2020-11-04T14:51:54-05:00
Actually add tests

- - - - -


4 changed files:

- compiler/GHC/Tc/Utils/Unify.hs
- + testsuite/tests/typecheck/should_compile/CbvOverlap.hs
- + testsuite/tests/typecheck/should_compile/InstanceGivenOverlap.hs
- + testsuite/tests/typecheck/should_compile/InstanceGivenOverlap2.hs


Changes:

=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -1502,14 +1502,12 @@ lhsPriority tv
 
 {- Note [TyVar/TyVar orientation]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-"RAE": Update
-
 Given (a ~ b), should we orient the CEqCan as (a~b) or (b~a)?
 This is a surprisingly tricky question! This is invariant (TyEq:TV).
 
-The question is answered by swapOverTyVars, which is use
+The question is answered by swapOverTyVars, which is used
   - in the eager unifier, in GHC.Tc.Utils.Unify.uUnfilledVar1
-  - in the constraint solver, in GHC.Tc.Solver.Canonical.canEqTyVarHomo
+  - in the constraint solver, in GHC.Tc.Solver.Canonical.canEqCanLHS2
 
 First note: only swap if you have to!
    See Note [Avoid unnecessary swaps]
@@ -1529,15 +1527,23 @@ So we look for a positive reason to swap, using a three-step test:
         looks for meta tyvars on the left
 
   Tie-breaking rules for MetaTvs:
-  - TauTv = 3: if we have  tyv_tv ~ tau_tv,
-       put tau_tv on the left because there are fewer
-       restrictions on updating TauTvs.  Or to say it another
-       way, then we won't lose the TyVarTv flag
+  - CycleBreakerTv: This is essentially a stand-in for another type;
+       it's untouchable and should have the same priority as a skolem: 0.
+
+  - TyVarTv: These can unify only with another tyvar, but we can't unify
+       a TyVarTv with a TauTv, because then the TyVarTv could (transitively)
+       get a non-tyvar type. So give these a low priority: 1.
+
+  - TauTv: This is the common case; we want these on the left so that they
+       can be written to: 2.
 
-  - TyVarTv = 2: TyVarTvs come next
+  - RuntimeUnkTv: These aren't really meta-variables used in type inference,
+       but just a convenience in the implementation of the GHCi debugger.
+       Eagerly write to these: 3. See Note [RuntimeUnkTv] in
+       GHC.Runtime.Heap.Inspect.
 
 * Names. If the level and priority comparisons are all
-  equal, try to eliminate a TyVars with a System Name in
+  equal, try to eliminate a TyVar with a System Name in
   favour of ones with a Name derived from a user type signature
 
 * Age.  At one point in the past we tried to break any remaining


=====================================
testsuite/tests/typecheck/should_compile/CbvOverlap.hs
=====================================
@@ -0,0 +1,16 @@
+{-# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts #-}
+
+module CbvOverlap where
+
+-- This is concerned with Note [Type variable cycles in Givens] and class lookup
+
+class C a where
+  meth :: a -> ()
+
+instance C Int where
+  meth _ = ()
+
+type family F a
+
+foo :: C (F a) => a -> Int -> ()
+foo _ n = meth n


=====================================
testsuite/tests/typecheck/should_compile/InstanceGivenOverlap.hs
=====================================
@@ -0,0 +1,23 @@
+{-# LANGUAGE ScopedTypeVariables, FlexibleInstances, MultiParamTypeClasses,
+             TypeFamilies, FlexibleContexts, AllowAmbiguousTypes #-}
+
+module InstanceGivenOverlap where
+
+-- See Note [Instance and Given overlap] in GHC.Tc.Solver.Interact.
+-- This tests the Note when the Wanted contains a type family.
+
+class P a
+class Q a
+class R a b
+
+instance P x => Q [x]
+instance (x ~ y) => R y [x]
+
+type family F a b where
+  F [a] a = a
+
+wob :: forall a b. (Q [F a b], R b a) => a -> Int
+wob = undefined
+
+g :: forall a. Q [a] => [a] -> Int
+g x = wob x


=====================================
testsuite/tests/typecheck/should_compile/InstanceGivenOverlap2.hs
=====================================
@@ -0,0 +1,44 @@
+{-# LANGUAGE ScopedTypeVariables, AllowAmbiguousTypes, TypeApplications,
+             TypeFamilies, PolyKinds, DataKinds, FlexibleInstances,
+             MultiParamTypeClasses, FlexibleContexts, PartialTypeSignatures #-}
+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
+
+module InstanceGivenOverlap2 where
+
+import Data.Proxy
+
+class P a
+class Q a
+class R a b
+
+newtype Tagged (t :: k) a = Tagged a
+
+type family F a
+type instance F (Tagged @Bool t a) = [a]
+
+instance P x => Q [x]
+instance (x ~ y) => R y [x]
+
+wob :: forall a b. (Q [b], R b a) => a -> Int
+wob = undefined
+
+it'sABoolNow :: forall (t :: Bool). Int
+it'sABoolNow = undefined
+
+class HasBoolKind t
+instance k ~ Bool => HasBoolKind (t :: k)
+
+it'sABoolLater :: forall t. HasBoolKind t => Int
+it'sABoolLater = undefined
+
+g :: forall t a. Q (F (Tagged t a)) => Proxy t -> [a] -> _
+g _ x = it'sABoolNow @t + wob x
+
+g2 :: forall t a. Q (F (Tagged t a)) => Proxy t -> [a] -> _
+g2 _ x = wob x + it'sABoolNow @t
+
+g3 :: forall t a. Q (F (Tagged t a)) => Proxy t -> [a] -> _
+g3 _ x = it'sABoolLater @t + wob x
+
+g4 :: forall t a. Q (F (Tagged t a)) => Proxy t -> [a] -> _
+g4 _ x = wob x + it'sABoolLater @t



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/ebfebd6fd6e6407bc0c8ad81d31616b76fc8ce3d...9d122639ed288a794ffa20dae3ba9721f319c004

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/ebfebd6fd6e6407bc0c8ad81d31616b76fc8ce3d...9d122639ed288a794ffa20dae3ba9721f319c004
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/20201104/42943963/attachment-0001.html>