-
Notifications
You must be signed in to change notification settings - Fork 37
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Browse files
Browse the repository at this point in the history
- Loading branch information
1 parent
4af2361
commit 4772247
Showing
5 changed files
with
52 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,40 @@ | ||
Singletons/T376.hs:(0,0)-(0,0): Splicing declarations | ||
singletons | ||
[d| f :: (() -> ()) -> (() -> ()) | ||
f g = g :: () -> () |] | ||
======> | ||
f :: (() -> ()) -> () -> () | ||
f g = g :: () -> () | ||
type FSym2 (a0123456789876543210 :: (~>) () ()) (a0123456789876543210 :: ()) = | ||
F a0123456789876543210 a0123456789876543210 | ||
instance SuppressUnusedWarnings (FSym1 a0123456789876543210) where | ||
suppressUnusedWarnings = snd (((,) FSym1KindInference) ()) | ||
data FSym1 (a0123456789876543210 :: (~>) () ()) :: (~>) () () | ||
where | ||
FSym1KindInference :: forall a0123456789876543210 | ||
a0123456789876543210 | ||
arg. SameKind (Apply (FSym1 a0123456789876543210) arg) (FSym2 a0123456789876543210 arg) => | ||
FSym1 a0123456789876543210 a0123456789876543210 | ||
type instance Apply (FSym1 a0123456789876543210) a0123456789876543210 = F a0123456789876543210 a0123456789876543210 | ||
instance SuppressUnusedWarnings FSym0 where | ||
suppressUnusedWarnings = snd (((,) FSym0KindInference) ()) | ||
data FSym0 :: (~>) ((~>) () ()) ((~>) () ()) | ||
where | ||
FSym0KindInference :: forall a0123456789876543210 | ||
arg. SameKind (Apply FSym0 arg) (FSym1 arg) => | ||
FSym0 a0123456789876543210 | ||
type instance Apply FSym0 a0123456789876543210 = FSym1 a0123456789876543210 | ||
type family F (a :: (~>) () ()) (a :: ()) :: () where | ||
F g a_0123456789876543210 = Apply (g :: (~>) () ()) a_0123456789876543210 | ||
sF :: | ||
forall (t :: (~>) () ()) (t :: ()). | ||
Sing t -> Sing t -> Sing (Apply (Apply FSym0 t) t :: ()) | ||
sF | ||
(sG :: Sing g) | ||
(sA_0123456789876543210 :: Sing a_0123456789876543210) | ||
= (applySing (sG :: Sing (g :: (~>) () ()))) sA_0123456789876543210 | ||
instance SingI (FSym0 :: (~>) ((~>) () ()) ((~>) () ())) where | ||
sing = (singFun2 @FSym0) sF | ||
instance SingI d => | ||
SingI (FSym1 (d :: (~>) () ()) :: (~>) () ()) where | ||
sing = (singFun1 @(FSym1 (d :: (~>) () ()))) (sF (sing @d)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
module T376 where | ||
|
||
import Data.Singletons.TH | ||
|
||
$(singletons [d| | ||
f :: (() -> ()) -> (() -> ()) | ||
f g = g :: () -> () | ||
|]) |