content: {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE UndecidableInstances #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE AllowAmbiguousTypes #-}  -- 'c' is ambiguous
  
  module T8566 where
  
  import Data.Kind (Type)
  
  data U (s :: Type) = forall v. AA v [U s]
  -- AA :: forall (s:*) (v:*). v -> [U s] -> U s
  
  data I (u :: U Type) (r :: [Type]) :: Type where
     A :: I (AA t as) r                  -- Existential k
  
  -- A :: forall (u:U *) (r:[*])                  Universal
  --             (k:BOX) (t:k) (as:[U *]).        Existential
  --             (u ~ AA * k t as) =>
  --             I u r
  
  -- fs unused, but needs to be present for the bug
  class C (u :: U Type) (r :: [Type]) (fs :: [Type]) where
     c :: I u r -> I u r
  
  -- c :: forall (u :: U *) (r :: [*]) (fs :: [*]). C u r fs => I u r -> I u r
  
  instance (C (AA (t (I a ps)) as) ps fs) => C (AA t (a ': as)) ps fs where
  -- instance C (AA t (a ': as)) ps fs where
    c A = c undefined
  