[Git][ghc/ghc][wip/cfuneqcan-refactor] Super skolems are really super.

[Richard Eisenberg]

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


Commits:
cbdfe1b9 by Richard Eisenberg at 2020-10-11T16:42:36-04:00
Super skolems are really super.

- - - - -


2 changed files:

- compiler/GHC/Core/Coercion/Opt.hs
- compiler/GHC/Core/Unify.hs


Changes:

=====================================
compiler/GHC/Core/Coercion/Opt.hs
=====================================
@@ -27,7 +27,6 @@ import GHC.Types.Var.Env
 import GHC.Data.Pair
 import GHC.Data.List.SetOps ( getNth )
 import GHC.Core.Unify
-import GHC.Core.InstEnv
 import Control.Monad   ( zipWithM )
 
 import GHC.Utils.Outputable
@@ -1002,7 +1001,7 @@ checkAxInstCo (AxiomInstCo ax ind cos)
     check_no_conflict _    [] = Nothing
     check_no_conflict flat (b at CoAxBranch { cab_lhs = lhs_incomp } : rest)
          -- See Note [Apartness] in GHC.Core.FamInstEnv
-      | SurelyApart <- tcUnifyTysFG instanceBindFun flat lhs_incomp
+      | SurelyApart <- tcUnifyTysFG (const BindMe) flat lhs_incomp
       = check_no_conflict flat rest
       | otherwise
       = Just b


=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -366,9 +366,29 @@ indexed-types/should_compile/Overlap14.
 Note [Unification with skolems]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 If we discover that two types unify if and only if a skolem variable is
-substituted, we can't properly unify the types. But, that skolem variable
-may later be instantiated with a unifyable type. So, we return maybeApart
-in these cases.
+substituted, we can't properly unify the types. Perhaps surprisingly,
+we say that these types are SurelyApart. This is to allow an example
+like the following:
+
+  class C a b where
+    meth :: a -> b -> ()
+
+  instance C a a where ...
+  instance C a Int where
+    meth = meth   -- a bit silly, but this is meant to be a small example
+
+NB: No -XOverlappingInstances or overlapp(ing|able|ed) pragmas.
+
+The recursive call within the definition of `meth` is actually ambiguous:
+if the instance variable `a` becomes Int, then the first instance would
+match. But this is silly, because if `a` were Int, then we would never
+have ended up in the second instance in the first place.
+
+We thus say that an unbindable variable is SurelyApart from other
+types. This allows us to accept the program above.
+
+See also Note [Binding when looking up instances] in GHC.Core.InstEnv.
+
 -}
 
 -- | Simple unification of two types; all type variables are bindable
@@ -1163,12 +1183,12 @@ uUnrefined env tv1' ty2 ty2' kco
              -- How could this happen? If we're only matching and if
              -- we're comparing forall-bound variables.
 
-           _ -> maybeApart -- See Note [Unification with skolems]
+           _ -> surelyApart -- See Note [Unification with skolems]
   }}}}
 
 uUnrefined env tv1' ty2 _ kco -- ty2 is not a type variable
   = case tvBindFlag env tv1' of
-      Skolem -> maybeApart  -- See Note [Unification with skolems]
+      Skolem -> surelyApart  -- See Note [Unification with skolems]
       BindMe -> bindTv env tv1' (ty2 `mkCastTy` mkSymCo kco)
 
 bindTv :: UMEnv -> OutTyVar -> Type -> UM ()



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/cbdfe1b9957e3c1f83feaf10e344e21864c202f2
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/20201011/48aace45/attachment-0001.html>