...
 
Commits (1)
  • Simon Peyton Jones's avatar
    Significant refactor of Lint · 92cbc212
    Simon Peyton Jones authored
    This refactoring of Lint was triggered by #17923, which is
    fixed by this patch.
    
    The main change is this.  Instead of
       lintType :: Type -> LintM LintedKind
    we now have
       lintType :: Type -> LintM LintedType
    
    Previously, all of typeKind was effectively duplicate in lintType.
    Moreover, since we have an ambient substitution, we still had to
    apply the substition here and there, sometimes more than once. It
    was all very tricky, in the end, and made my head hurt.
    
    Now, lintType returns a fully linted type, with all substitutions
    performed on it.  This is much simpler.
    
    The same thing is needed for Coercions.  Instead of
      lintCoercion :: OutCoercion
                   -> LintM (LintedKind, LintedKind,
                             LintedType, LintedType, Role)
    we now have
      lintCoercion :: Coercion -> LintM LintedCoercion
    
    Much simpler!  The code is shorter and less bug-prone.
    
    There are a lot of knock on effects.  But life is now better.
    92cbc212
This diff is collapsed.
......@@ -2447,7 +2447,7 @@ normally it would make no sense to have
forall r. (ty :: K r)
because the kind of the forall would escape the binding
of 'r'. But in this case it's fine because (K r) exapands
to Type, so we expliclity /permit/ the type
to Type, so we explicitly /permit/ the type
forall r. T r
To accommodate such a type, in typeKind (forall a.ty) we use
......@@ -2455,8 +2455,13 @@ occCheckExpand to expand any type synonyms in the kind of 'ty'
to eliminate 'a'. See kinding rule (FORALL) in
Note [Kinding rules for types]
And in TcValidity.checkEscapingKind, we use also use
occCheckExpand, for the same reason.
See also
* TcUnify.occCheckExpand
* GHC.Core.Utils.coreAltsType
* TcValidity.checkEscapingKind
all of which grapple with with the same problem.
See #14939.
-}
-----------------------------
......
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wall #-}
module Bug where
import Data.Kind
-- type SingFunction2 f = forall t1 t2. Sing t1 -> Sing t2 -> Sing (f `Apply` t1 `Apply` t2)
type SingFunction2 f = forall t1. Sing t1 -> forall t2. Sing t2 -> Sing (f `Apply` t1 `Apply` t2)
singFun2 :: forall f. SingFunction2 f -> Sing f
singFun2 f = SLambda (\x -> SLambda (f x))
type family Sing :: k -> Type
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: a ~> b) (x :: a) :: b
data Sym4 a
data Sym3 a
type instance Apply Sym3 _ = Sym4
newtype SLambda (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }
type instance Sing = SLambda
und :: a
und = undefined
data E
data ShowCharSym0 :: E ~> E ~> E
sShow_tuple :: SLambda Sym4
sShow_tuple
= applySing (singFun2 @Sym3 und)
(und (singFun2 @Sym3
(und (applySing (singFun2 @Sym3 und)
(applySing (singFun2 @ShowCharSym0 und) und)))))
......@@ -294,3 +294,4 @@ test('T16828', normal, compile, [''])
test('T17008b', normal, compile, [''])
test('T17056', normal, compile, [''])
test('T17405', normal, multimod_compile, ['T17405c', '-v0'])
test('T17923', normal, compile, [''])