Commit 2745dfb5 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Test Trac #9144

parent fb74d717
{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, GADTs, RankNTypes #-}
module T9144 where
import Data.Proxy
import GHC.TypeLits
data family Sing (a :: k)
data SomeSing :: KProxy k -> * where
SomeSing :: forall (a :: k). Sing a -> SomeSing ('KProxy :: KProxy k)
class kproxy ~ 'KProxy => SingKind (kproxy :: KProxy k) where
fromSing :: forall (a :: k). Sing a -> DemoteRep ('KProxy :: KProxy k)
toSing :: DemoteRep ('KProxy :: KProxy k) -> SomeSing ('KProxy :: KProxy k)
type family DemoteRep (kproxy :: KProxy k) :: *
data Foo = Bar Nat
data FooTerm = BarTerm Integer
data instance Sing (x :: Foo) where
SBar :: Sing n -> Sing (Bar n)
type instance DemoteRep ('KProxy :: KProxy Nat) = Integer
type instance DemoteRep ('KProxy :: KProxy Foo) = FooTerm
instance SingKind ('KProxy :: KProxy Nat) where
fromSing = undefined
toSing = undefined
instance SingKind ('KProxy :: KProxy Foo) where
fromSing (SBar n) = BarTerm (fromSing n)
toSing n = case toSing n of SomeSing n' -> SomeSing (SBar n')
T9144.hs:34:26:
Couldn't match type ‘Integer’ with ‘FooTerm’
Expected type: DemoteRep 'KProxy
Actual type: DemoteRep 'KProxy
In the first argument of ‘toSing’, namely ‘n’
In the expression: toSing n
......@@ -101,3 +101,4 @@ test('T7481', normal, compile_fail,[''])
test('T8705', normal, compile, [''])
test('T8985', normal, compile, [''])
test('T9106', normal, compile_fail, [''])
test('T9144', normal, compile_fail, [''])
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment