Re: [GHC] #15472: GHC HEAD type inference regression post-"Remove decideKindGeneralisationPlan"

3 Aug 2018

      #15472: GHC HEAD type inference regression post-"Remove
decideKindGeneralisationPlan"
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  highest           |            Milestone:  8.8.1
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |
      Resolution:  invalid           |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Actually, here is an ever-so-slightly smaller way to trigger the issue
 (which I also discovered in `singletons`)

 {{{#!hs
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 module Bug where

 import Data.Kind
 import Data.List.NonEmpty (NonEmpty(..))

 data TyFun :: Type -> Type -> Type
 type a ~> b = TyFun a b -> Type
 infixr 0 ~>
 type family Apply (f :: k1 ~> k2) (x :: k1) :: k2

 data family Sing :: forall k. k -> Type
 data instance Sing :: forall a. [a] -> Type where
   SNil  :: Sing '[]
   SCons :: Sing x -> Sing xs -> Sing (x:xs)
 data instance Sing :: forall a. NonEmpty a -> Type where
   (:%|) :: Sing x -> Sing xs -> Sing (x :| xs)

 type family LetGo x xs b cs where
   LetGo x xs b (c:cs) = b <> LetGo x xs c cs
   LetGo x xs b '[]    = b

 type family SconcatDefault (arg :: NonEmpty a) :: a where
   SconcatDefault (x :| xs) = LetGo x xs x xs

 class PSemigroup (a :: Type) where
   type (<>) (arg1 :: a) (arg2 :: a) :: a
   type Sconcat (arg :: NonEmpty a) :: a
   type Sconcat arg = SconcatDefault arg

 class SSemigroup a where
   (%<>) :: forall (t1 :: a) (t2 :: a).
            Sing t1 -> Sing t2 -> Sing (t1 <> t2 :: a)
   sSconcat         :: forall (t :: NonEmpty a).
                       Sing t -> Sing (Sconcat t :: a)
   default sSconcat :: forall (t :: NonEmpty a).
                       (Sconcat t :: a) ~ SconcatDefault t
                    => Sing t -> Sing (Sconcat t :: a)
   sSconcat ((sA :: Sing x) :%| (sAs :: Sing xs))
     = let sGo :: forall arg1 arg2.
                  Sing arg1 -> Sing arg2 -> Sing (LetGo x xs arg1 arg2)
           sGo sB (SCons sC sCs) = sB %<> sGo sC sCs
           sGo sB SNil = sB
       in sGo sA sAs
 }}}

 This typechecks in GHC 8.4/8.6 but fails in HEAD with:

 {{{
 $ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:48:35: error:
     • Could not deduce (SSemigroup k) arising from a use of ‘%<>’
       from the context: SSemigroup a
         bound by the class declaration for ‘SSemigroup’ at Bug.hs:37:7-16
       or from: Sconcat t ~ SconcatDefault t
         bound by the type signature for:
                    sSconcat :: forall (t :: NonEmpty a).
                                (Sconcat t ~ SconcatDefault t) =>
                                Sing t -> Sing (Sconcat t)
         at Bug.hs:(42,23)-(44,53)
       or from: t ~ (x ':| xs)
         bound by a pattern with constructor:
                    :%| :: forall a (x :: a) (xs :: [a]).
                           Sing x -> Sing xs -> Sing (x ':| xs),
                  in an equation for ‘sSconcat’
         at Bug.hs:45:13-47
       or from: arg2 ~ (x1 : xs1)
         bound by a pattern with constructor:
                    SCons :: forall a (x :: a) (xs :: [a]).
                             Sing x -> Sing xs -> Sing (x : xs),
                  in an equation for ‘sGo’
         at Bug.hs:48:19-30
       Possible fix:
         add (SSemigroup k) to the context of
           the data constructor ‘SCons’
           or the type signature for:
                sGo :: forall k (arg1 :: k) (arg2 :: [k]).
                       Sing arg1 -> Sing arg2 -> Sing (LetGo x xs arg1
 arg2)
     • In the expression: sB %<> sGo sC sCs
       In an equation for ‘sGo’: sGo sB (SCons sC sCs) = sB %<> sGo sC sCs
       In the expression:
         let
           sGo ::
             forall arg1 arg2.
             Sing arg1 -> Sing arg2 -> Sing (LetGo x xs arg1 arg2)
           sGo sB (SCons sC sCs) = sB %<> sGo sC sCs
           sGo sB SNil = sB
         in sGo sA sAs
    |
 48 |           sGo sB (SCons sC sCs) = sB %<> sGo sC sCs
    |                                   ^^^^^^^^^^^^^^^^^
 }}}

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15472#comment:6
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler