blob: d9b8a996572d0fa088f14c6331c1907897c5d239 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module T12845 where
import Data.Proxy
data Foo (m :: Bool)
type family Head (xs :: [(Bool, Bool)]) where Head (x ': xs) = x
type family Bar (x :: Bool) (y :: Bool) :: Bool
-- to trigger the bug, r and r' cannot *both* appear on the RHS
broken :: forall r r' rngs . ('(r,r') ~ Head rngs, Bar r r' ~ 'True, _)
=> Foo r -> Proxy rngs -> ()
broken x _ = let y = requireBar x :: Foo r' in ()
requireBar :: (Bar m m' ~ 'True) => Foo m -> Foo m'
requireBar = undefined
|
