Commit 92cbc212 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Significant refactor of Lint

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.
parent 2643ba46
Pipeline #17179 failed with stages
in 209 minutes and 53 seconds
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
= 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, [''])
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