[Git][ghc/ghc][wip/derived-refactor] More checkpoint. Moar.

[Richard Eisenberg]

Richard Eisenberg pushed to branch wip/derived-refactor at Glasgow Haskell Compiler / GHC


Commits:
24f51ff6 by Richard Eisenberg at 2020-09-18T15:58:28-04:00
More checkpoint. Moar.

- - - - -


1 changed file:

- + testsuite/tests/dependent/should_compile/LopezJuan.hs


Changes:

=====================================
testsuite/tests/dependent/should_compile/LopezJuan.hs
=====================================
@@ -0,0 +1,57 @@
+{-
+
+This test is inspired by
+  Practical dependent type checking using twin types
+  Victor López Juan and Nils Anders Danielsson
+  TyDe '20
+  https://dl.acm.org/doi/10.1145/3406089.3409030
+-}
+
+{-# LANGUAGE TypeOperators, TypeApplications, DataKinds,
+             StandaloneKindSignatures, PolyKinds, GADTs,
+             TypeFamilies #-}
+
+module LopezJuan where
+
+import Data.Type.Equality ( (:~~:)(..) )
+import Data.Kind ( Type )
+
+-- amazingly, this worked without modification
+
+data SBool :: Bool -> Type where
+  SFalse :: SBool False
+  STrue  :: SBool True
+
+data BoolOp where
+  None :: Bool -> BoolOp
+  Some :: Bool -> BoolOp
+
+type F :: Bool -> Type
+type family F b
+
+get :: BoolOp -> Bool
+get (None _) = True
+get (Some x) = x
+
+type Get :: BoolOp -> Bool
+type family Get x where
+  Get (None _) = True
+  Get (Some x) = x
+
+type TyFun :: Type -> Type -> Type
+data TyFun arg res
+
+type (~>) :: Type -> Type -> Type
+type arg ~> res = TyFun arg res -> Type
+infixr 0 ~>
+
+type (@@) :: (a ~> b) -> a -> b
+type family f @@ arg
+
+data Const :: a -> (b ~> a)
+
+f :: SBool x -> (:~~:) @(F (Get (_alpha x)) ~> BoolOp)
+                       @(F True ~> BoolOp)
+                       (Const (None x))
+                       (Const (_alpha x))
+f _ = HRefl



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/24f51ff65369485ec23bf24d8d0f6b207598e7a5

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/24f51ff65369485ec23bf24d8d0f6b207598e7a5
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200918/5c6cf2b2/attachment-0001.html>