GHC 8.4.1-alpha regression with TypeInType

[RyanGlScott]

GHC 8.2.2 is able to typecheck this code:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module SGenerics where

import Data.Kind (Type)
import Data.Type.Equality ((:~:)(..), sym, trans)
import Data.Void

data family Sing (z :: k)

class Generic (a :: Type) where
    type Rep a :: Type
    from :: a -> Rep a
    to :: Rep a -> a

class PGeneric (a :: Type) where
  type PFrom (x :: a)     :: Rep a
  type PTo   (x :: Rep a) :: a

class SGeneric k where
  sFrom :: forall (a :: k).     Sing a -> Sing (PFrom a)
  sTo   :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k)

class (PGeneric k, SGeneric k) => VGeneric k where
  sTof  :: forall (a :: k).     Sing a -> PTo (PFrom a) :~: a
  sFot  :: forall (a :: Rep k). Sing a -> PFrom (PTo a :: k) :~: a

data Decision a = Proved a
                | Disproved (a -> Void)

class SDecide k where
  (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
  default (%~) :: forall (a :: k) (b :: k). (VGeneric k, SDecide (Rep k))
               => Sing a -> Sing b -> Decision (a :~: b)
  s1 %~ s2 = case sFrom s1 %~ sFrom s2 of
    Proved (Refl :: PFrom a :~: PFrom b) ->
      case (sTof s1, sTof s2) of
          (Refl, Refl) -> Proved Refl
    Disproved contra -> Disproved (\Refl -> contra Refl)

But GHC 8.4.1-alpha2 cannot:

$ /opt/ghc/8.4.1/bin/ghc Bug.hs
[1 of 1] Compiling SGenerics        ( Bug.hs, Bug.o )

Bug.hs:44:52: error:
    • Could not deduce: PFrom a ~ PFrom a
      from the context: b ~ a
        bound by a pattern with constructor:
                   Refl :: forall k (a :: k). a :~: a,
                 in a lambda abstraction
        at Bug.hs:44:37-40
      Expected type: PFrom a :~: PFrom b
        Actual type: PFrom a :~: PFrom a
      NB: ‘PFrom’ is a non-injective type family
    • In the first argument of ‘contra’, namely ‘Refl’
      In the expression: contra Refl
      In the first argument of ‘Disproved’, namely
        ‘(\ Refl -> contra Refl)’
    • Relevant bindings include
        contra :: (PFrom a :~: PFrom b) -> Void (bound at Bug.hs:44:15)
        s2 :: Sing b (bound at Bug.hs:40:9)
        s1 :: Sing a (bound at Bug.hs:40:3)
        (%~) :: Sing a -> Sing b -> Decision (a :~: b)
          (bound at Bug.hs:40:3)
   |
44 |     Disproved contra -> Disproved (\Refl -> contra Refl)
   |                                                    ^^^^

[RyanGlScott]

This regression was introduced in commit 8e15e3d370e9c253ae0dbb330e25b72cb00cdb76 (Improve error messages around kind mismatches.).

I'm unsure if this is related to #14038 (which was also triggered by the same commit).

[goldfire]

I'm pretty sure this is #12919. It works on my branch, held up due to performance problems. It's being actively worked on by @alexvieth, to whom I've gratefully delegated fixing those performance problems. But when I say active, I mean it: Alex sent me some results offline this morning.

[monoidal]

For the record, here's a smaller test case:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module SGenerics where

import Data.Kind (Type)

type family R :: Type
data family Sing (z :: R)
type family PFrom (x :: Type) :: R

u :: forall (a :: R). Sing a
u = u

v :: forall (a :: Type). Sing (PFrom a)
v = u

[Richard Eisenberg <rae@…>]

In e3dbb44f/ghc:

Fix #12919 by making the flattener homegeneous.

This changes a key invariant of the flattener. Previously,
flattening a type meant flattening its kind as well. But now,
flattening is always homogeneous -- that is, the kind of the
flattened type is the same as the kind of the input type.
This is achieved by various wizardry in the TcFlatten.flatten_many
function, as described in Note [flatten_many].

There are several knock-on effects, including some refactoring
in the canonicalizer to take proper advantage of the flattener's
changed behavior. In particular, the tyvar case of can_eq_nc' no
longer needs to take casts into account.

Another effect is that flattening a tyconapp might change it
into a casted tyconapp. This might happen if the result kind
of the tycon contains a variable, and that variable changes
during flattening. Because the flattener is homogeneous, it tacks
on a cast to keep the tyconapp kind the same. However, this
is problematic when flattening CFunEqCans, which need to have
an uncasted tyconapp on the LHS and must remain homogeneous.
The solution is a more involved canCFunEqCan, described in
Note [canCFunEqCan].

This patch fixes #13643 (as tested in typecheck/should_compile/T13643)
and the panic in typecheck/should_compile/T13822 (as reported in #14024).
Actually, there were two bugs in T13822: the first was just some
incorrect logic in tryFill (part of the unflattener) -- also fixed
in this patch -- and the other was the main bug fixed in this ticket.

The changes in this patch exposed a long-standing flaw in OptCoercion,
in that breaking apart an AppCo sometimes has unexpected effects on
kinds. See new Note [EtaAppCo] in OptCoercion, which explains the
problem and fix.

Also here is a reversion of the major change in
09bf135ace55ce2572bf4168124d631e386c64bb, affecting ctEvCoercion.
It turns out that making the flattener homogeneous changes the
invariants on the algorithm, making the change in that patch
no longer necessary.

This patch also fixes:
  #14038 (dependent/should_compile/T14038)
  #13910 (dependent/should_compile/T13910)
  #13938 (dependent/should_compile/T13938)
  #14441 (typecheck/should_compile/T14441)
  #14556 (dependent/should_compile/T14556)
  #14720 (dependent/should_compile/T14720)
  #14749 (typecheck/should_compile/T14749)

Sadly, this patch negatively affects performance of type-family-
heavy code. The following patch fixes these performance degradations.
However, the performance fixes are somewhat invasive and so I've
kept them as a separate patch, labeling this one as [skip ci] so
that validation doesn't fail on the performance cases.