Summary

The following snippet (some of the code coming from generics-sop), either sends GHC into endless allocation loop (8.8), or produces a self-contradictory error message:

{-# LANGUAGE AllowAmbiguousTypes     #-}
{-# LANGUAGE DataKinds               #-}
{-# LANGUAGE FlexibleInstances       #-}
{-# LANGUAGE GADTs                   #-}
{-# LANGUAGE KindSignatures          #-}
{-# LANGUAGE PolyKinds               #-}
{-# LANGUAGE RankNTypes              #-}
{-# LANGUAGE TypeFamilies            #-}
{-# LANGUAGE ConstraintKinds         #-}
{-# LANGUAGE FlexibleContexts        #-}
{-# LANGUAGE MultiParamTypeClasses   #-}
{-# LANGUAGE TypeOperators           #-}
{-# LANGUAGE UndecidableInstances    #-}
{-# LANGUAGE UndecidableSuperClasses #-}

import Data.Kind (Constraint)
import Data.Proxy (Proxy)
import Data.Typeable (Typeable)

-- First, `generics-sop` code, intact.
--
type family
  AllF (c :: k -> Constraint) (xs :: [k]) :: Constraint where
  AllF _c '[]       = ()
  AllF  c (x ': xs) = (c x, All c xs)

class (AllF c xs, SListI xs) => All (c :: k -> Constraint) (xs :: [k])
instance All c '[]
instance (c x, All c xs) => All c (x ': xs) where

class Top x
instance Top x

type SListI = All Top

-- Next, user code, minimised.
--
data GADT
  = forall (xs :: [*]) (a :: *)
    . (Top a, All Typeable xs)
    => GADT

withSomePipe'
  :: GADT
  -> (forall (xs :: [*])
      . (Proxy xs -> GADT)
      -> GADT)
  -> GADT
withSomePipe' GADT f = f (const GADT)

8.10.1 says there are overlapping instances, but only lists one, which isn't terribly surprising, as there is indeed just one instance for Top:

[nix-shell:~/lift]$ ghc ~/ghc-instance-self-overlapping[ghc-instance-self-overlapping.hs](/uploads/adca7101458489bc35d16ceaf00af943/ghc-instance-self-overlapping.hs).hs
[1 of 1] Compiling Main             ( /home/desktop/repro.hs, /home/desktop/repro.o )

/home/desktop/repro.hs:1:1: error:
    The IO action `main' is not defined in module `Main'
  |
1 | {-# LANGUAGE AllowAmbiguousTypes     #-}
  | ^

/home/desktop/repro.hs:45:33: error:
    * Overlapping instances for Top a0 arising from a use of `GADT'
      Matching givens (or their superclasses):
        Top a
          bound by a pattern with constructor:
                     GADT :: forall (xs :: [*]) a. (Top a, All Typeable xs) => GADT,
                   in an equation for withSomePipe'
          at /home/desktop/repro.hs:45:15-18
      Matching instances:
        instance forall k (x :: k). Top x
          -- Defined at /home/desktop/repro.hs:30:10
      (The choice depends on the instantiation of `a0')
    * In the first argument of `const', namely `GADT'
      In the first argument of `f', namely `(const GADT)'
      In the expression: f (const GADT)
   |
45 | withSomePipe' GADT f = f (const GADT)

Steps to reproduce

With either ghc 8.10.1 or ghc 8.8.3:

ghc repro.hs

Expected behavior

The compiler shouldn't contradict itself in the error message, and it certainly needn't crash, although the latter part was fixed in the new release.

Environment

• GHC version used: 8.8.3 / 8.10.1

Optional:

• Operating System:
• System Architecture: