Commit 0a851903 authored by Simon Peyton Jones's avatar Simon Peyton Jones

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 18d0bdd3
   Author: Simon Peyton Jones <simonpj@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.
parent e3ec2e7a
......@@ -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
......
......@@ -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
......
......@@ -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
......
{-# 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) = (->)
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)’
......@@ -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, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment