[GHC] #14584: Core Lint error

15 Dec 2017


      #14584: Core Lint error
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 {{{#!hs
 {-# Language PartialTypeSignatures #-}
 {-# Language TypeFamilyDependencies, KindSignatures #-}
 {-# Language PolyKinds #-}
 {-# Language DataKinds #-}
 {-# Language TypeFamilies #-}
 {-# Language RankNTypes #-}
 {-# Language NoImplicitPrelude #-}
 {-# Language FlexibleContexts #-}
 {-# Language MultiParamTypeClasses #-}
 {-# Language GADTs #-}
 {-# Language ConstraintKinds #-}
 {-# Language FlexibleInstances #-}
 {-# Language TypeOperators #-}
 {-# Language ScopedTypeVariables #-}
 {-# Language DefaultSignatures #-}
 {-# Language FunctionalDependencies #-}
 {-# Language UndecidableSuperClasses #-}
 {-# Language UndecidableInstances #-}
 {-# Language TypeInType #-}
 {-# Language AllowAmbiguousTypes #-}
 {-# Language InstanceSigs, TypeApplications #-}

 import Data.Monoid
 import Data.Kind

 data family Sing (a::k)

 class SingKind k where
   type Demote k = (res :: Type) | res -> k
   fromSing :: Sing (a::k) -> Demote k

 class SingI (a::k) where
   sing :: Sing a

 data ACT  :: Type -> Type -> Type
 data MHOM :: Type -> Type -> Type

 type m ·-  a  = ACT  m a  -> Type
 type m ·-> m' = MHOM m m' -> Type

 class Monoid m => Action (act :: m ·- a) where
   act :: m -> (a -> a)

 class (Monoid m, Monoid m') => MonHom (mhom :: m ·-> m') where
   monHom :: m -> m'

 data MonHom_Distributive m :: (m ·- a) -> (a ·-> a)

 type Good k = (Demote k ~ k, SingKind k)

 instance (Action act, Monoid a, Good m) => MonHom (MonHom_Distributive m
 act :: a ·-> a) where
   monHom :: a -> a
   monHom = act @_ @_ @act (fromSing @m (sing @m @a :: Sing _)) where
 }}}

 fails on 8.2.1 and 8.3.20171208 when passed `-fdefer-type-errors -dcore-
 lint`, full log attached

 {{{
 $ ghci -ignore-dot-ghci -fdefer-type-errors -dcore-lint 146-bug.hs
 GHCi, version 8.3.20171208: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( 146-bug.hs, interpreted )
 *** Core Lint errors : in result of Desugar (after optimization) ***
 <no location info>: warning:
     In the expression: fromSing
                          @ m_a2Ju
 ...
 }}}

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14584
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler