[Git][ghc/ghc][wip/cfuneqcan-refactor] Kill off Note [Unification with skolems]

[Richard Eisenberg]

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


Commits:
11802fc3 by Richard Eisenberg at 2020-11-24T15:04:23-05:00
Kill off Note [Unification with skolems]

- - - - -


3 changed files:

- compiler/GHC/Core/InstEnv.hs
- compiler/GHC/Core/Unify.hs
- compiler/GHC/Tc/Solver/Rewrite.hs


Changes:

=====================================
compiler/GHC/Core/InstEnv.hs
=====================================
@@ -1044,7 +1044,9 @@ isOverlappableTyVar, and the use of Skolem in instanceBindFun, above, means
 that these will be treated as fresh constants in the unification algorithm
 during instance lookup. Without this treatment, GHC would complain, saying
 that the choice of instance depended on the instantiation of 'a'; but of
-course it isn't *going* to be instantiated.
+course it isn't *going* to be instantiated. Note that it is necessary that
+the unification algorithm returns SurelyApart for these super-skolems
+for GHC to be able to commit to another instance.
 
 We do this only for super skolems.  For example we reject
         g :: forall a => [a] -> Int


=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -363,32 +363,6 @@ types are apart. This has practical consequences for the ability for closed
 type family applications to reduce. See test case
 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. 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
@@ -1193,12 +1167,12 @@ uUnrefined env tv1' ty2 ty2' kco
              -- How could this happen? If we're only matching and if
              -- we're comparing forall-bound variables.
 
-           _ -> surelyApart -- See Note [Unification with skolems]
+           _ -> surelyApart
   }}}}
 
 uUnrefined env tv1' ty2 _ kco -- ty2 is not a type variable
   = case tvBindFlag env tv1' of
-      Skolem -> surelyApart  -- See Note [Unification with skolems]
+      Skolem -> surelyApart
       BindMe -> bindTv env tv1' (ty2 `mkCastTy` mkSymCo kco)
 
 bindTv :: UMEnv -> OutTyVar -> Type -> UM ()
@@ -1242,6 +1216,8 @@ data BindFlag
   | Skolem      -- This type variable is a skolem constant
                 -- Don't bind it; it only matches itself
                 -- These variables are SurelyApart from other types
+                -- See Note [Binding when looking up instances] in GHC.Core.InstEnv
+                -- for why it must be SurelyApart.
   deriving Eq
 
 {-


=====================================
compiler/GHC/Tc/Solver/Rewrite.hs
=====================================
@@ -1023,6 +1023,6 @@ ty_con_binders_ty_binders' = foldr go ([], False)
     go (Bndr tv (NamedTCB vis)) (bndrs, _)
       = (Named (Bndr tv vis) : bndrs, True)
     go (Bndr tv (AnonTCB af))   (bndrs, n)
-      = (Anon af (unrestricted (tyVarKind tv))   : bndrs, n)
+      = (Anon af (tymult (tyVarKind tv)) : bndrs, n)
     {-# INLINE go #-}
 {-# INLINE ty_con_binders_ty_binders' #-}



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/11802fc3cb9d1a9bfe84193ed7f58508389f839c
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/20201124/ebaedffa/attachment-0001.html>