[commit: ghc] master: Fix a TyVar bug in the flattener (0a85190)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/0a85190312a1de3d300912051309b94589c08683/ghc

>---------------------------------------------------------------

commit 0a85190312a1de3d300912051309b94589c08683
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Tue Nov 14 09:16:22 2017 +0000

    Fix a TyVar bug in the flattener
    
    A year ago I gave up on trying to rigorously separate TyVars
    from TcTyVars, and instead allowed TyVars to appear rather more
    freely in types examined by the constraint solver:
    
       commit 18d0bdd3848201882bae167e3b15fd797d217e93
       Author: Simon Peyton Jones <simonpj at microsoft.com>
       Date:   Wed Nov 23 16:00:00 2016 +0000
    
       Allow TyVars in TcTypes
    
    See Note [TcTyVars in the typechecker] in TcType.
    
    However, TcFlatten.flatten_tyvar1 turned out to treat
    a TyVar specially, and implicitly assumed that it could
    not have an equality constraint in the inert set.  Wrong!
    
    This caused Trac #14450.  Fortunately it is easily fixed,
    by deleting code.


>---------------------------------------------------------------

0a85190312a1de3d300912051309b94589c08683
 compiler/typecheck/TcFlatten.hs         |  7 +------
 compiler/typecheck/TcType.hs            |  4 ++++
 compiler/typecheck/TcUnify.hs           |  2 +-
 testsuite/tests/polykinds/T14450.hs     | 31 +++++++++++++++++++++++++++++++
 testsuite/tests/polykinds/T14450.stderr |  8 ++++++++
 testsuite/tests/polykinds/all.T         |  1 +
 6 files changed, 46 insertions(+), 7 deletions(-)

diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index 3c44cde..c8479a6 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -1371,15 +1371,10 @@ flatten_tyvar1 :: TcTyVar -> FlatM FlattenTvResult
 -- See also the documentation for FlattenTvResult
 
 flatten_tyvar1 tv
-  | not (isTcTyVar tv)             -- Happens when flatten under a (forall a. ty)
-  = return FTRNotFollowed
-          -- So ty contains references to the non-TcTyVar a
-
-  | otherwise
   = do { mb_ty <- liftTcS $ isFilledMetaTyVar_maybe tv
-       ; role <- getRole
        ; case mb_ty of
            Just ty -> do { traceFlat "Following filled tyvar" (ppr tv <+> equals <+> ppr ty)
+                         ; role <- getRole
                          ; return (FTRFollowed ty (mkReflCo role ty)) } ;
            Nothing -> do { traceFlat "Unfilled tyvar" (ppr tv)
                          ; fr <- getFlavourRole
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 5e1e4be..d781aec 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -294,6 +294,10 @@ reasons:
     solve any kind equalities in foo's signature.  So the solver
     may see free occurrences of 'k'.
 
+    See calls to tcExtendTyVarEnv for other places that ordinary
+    TyVars are bought into scope, and hence may show up in the types
+    and inds generated by TcHsType.
+
 It's convenient to simply treat these TyVars as skolem constants,
 which of course they are.  So
 
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index 926db6e..0b2151b 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -1814,7 +1814,7 @@ matchExpectedFunKind hs_ty = go
     go k | Just k' <- tcView k = go k'
 
     go k@(TyVarTy kvar)
-      | isTcTyVar kvar, isMetaTyVar kvar
+      | isMetaTyVar kvar
       = do { maybe_kind <- readMetaTyVar kvar
            ; case maybe_kind of
                 Indirect fun_kind -> go fun_kind
diff --git a/testsuite/tests/polykinds/T14450.hs b/testsuite/tests/polykinds/T14450.hs
new file mode 100644
index 0000000..3b8f5b7
--- /dev/null
+++ b/testsuite/tests/polykinds/T14450.hs
@@ -0,0 +1,31 @@
+{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs #-}
+
+module T14450 where
+
+import Data.Kind
+
+data TyFun :: Type -> Type -> Type
+
+type a ~> b = TyFun a b -> Type
+
+type Cat ob = ob -> ob -> Type
+
+type SameKind (a :: k) (b :: k) = (() :: Constraint)
+
+type family Apply (f :: a ~> b) (x :: a) :: b where
+  Apply IddSym0 x = Idd x
+
+class Varpi (f :: i ~> j) where
+  type Dom (f :: i ~> j) :: Cat i
+  type Cod (f :: i ~> j) :: Cat j
+
+  varpa :: Dom f a a' -> Cod f (Apply f a) (Apply f a')
+
+type family Idd (a::k) :: k where
+  Idd (a::k) = a
+
+data IddSym0 :: k ~> k where
+  IddSym0KindInference :: IddSym0 l
+
+instance Varpi (IddSym0 :: k ~> k) where
+  type Dom (IddSym0 :: Type ~> Type) = (->)
diff --git a/testsuite/tests/polykinds/T14450.stderr b/testsuite/tests/polykinds/T14450.stderr
new file mode 100644
index 0000000..c7caf04
--- /dev/null
+++ b/testsuite/tests/polykinds/T14450.stderr
@@ -0,0 +1,8 @@
+
+T14450.hs:31:12: error:
+    • Expected kind ‘k ~> k’,
+        but ‘(IddSym0 :: Type ~> Type)’ has kind ‘* ~> *’
+    • In the first argument of ‘Dom’, namely
+        ‘(IddSym0 :: Type ~> Type)’
+      In the type instance declaration for ‘Dom’
+      In the instance declaration for ‘Varpi (IddSym0 :: k ~> k)’
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 66bd9b1..73408e8 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -173,3 +173,4 @@ test('T14265', normal, compile_fail, [''])
 test('T13391', normal, compile_fail, [''])
 test('T13391a', normal, compile, [''])
 test('T14270', normal, compile, [''])
+test('T14450', normal, compile_fail, [''])