GitLab

{-# 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
...

Trac metadata

Trac field	Value
Version	8.2.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture