1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
|
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeApplications #-}
--------------- The original bug report --------------
--
-- See T12734a for a smaller version
module T12734 where
import Prelude
import Data.Kind
import Control.Applicative
import Control.Monad.Fix
import Control.Monad.Trans.Identity
import Control.Monad.Trans.Class
import Control.Monad.IO.Class
data A
data B
data Net
data Ty
data Layer4 t l
data TermStore
-- Helpers: Stack
data Stack layers (t :: Type -> Type) where
SLayer :: t l -> Stack ls t -> Stack (l ': ls) t
SNull :: Stack '[] t
instance ( Constructor m (t l)
, Constructor m (Stack ls t)) => Constructor m (Stack (l ': ls) t)
instance Monad m => Constructor m (Stack '[] t)
-- Helpers: Expr
newtype Expr t layers = Expr (TermStack t layers)
type TermStack t layers = Stack layers (Layer4 (Expr t layers))
-- Helpers: Funny typeclass
class Monad m => Constructor m t
instance ( Monad m, expr ~ Expr t layers, Constructor m (TermStack t layers)
) => Constructor m (Layer4 expr Ty)
-- HERE IS A FUNNY BEHAVIOR: the commented line raises context reduction stack
-- overflow
test_gr ::
( Constructor m (TermStack t layers), Inferable A layers m, Inferable B t m
, bind ~ Expr t layers
-- ) => m (Expr t layers)
) => m bind
test_gr = undefined
-- Explicit information about a type which could be inferred
class Monad m => Inferable (cls :: Type) (t :: k) m | cls m -> t
newtype KnownTyx (cls :: Type) (t :: k) (m :: Type -> Type) (a :: Type) =
KnownTyx (IdentityT m a)
deriving (Show, Functor, Monad, MonadIO, MonadFix, MonadTrans,
Applicative, Alternative)
instance {-# OVERLAPPABLE #-} (t ~ t', Monad m) =>
Inferable cls t (KnownTyx cls t' m)
instance {-# OVERLAPPABLE #-} (Inferable cls t n, MonadTrans m, Monad (m n)) =>
Inferable cls t (m n)
runInferenceTx :: forall cls t m a. KnownTyx cls t m a -> m a
runInferenceTx = undefined
-- running it
test_ghc_err :: (MonadIO m, MonadFix m)
=> m (Expr Net '[Ty])
test_ghc_err = runInferenceTx @B @Net
$ runInferenceTx @A @'[Ty]
$ (test_gr)
|
