blob: c0bd01b85eb9c57ab011d050924d5689dbeb175a (
plain)
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
|
{-# LANGUAGE GADTs, TypeFamilies #-}
module T3851 where
import Data.Kind (Type)
type family TF a :: Type -> Type
type instance TF () = App (Equ ())
data Equ ix ix' where Refl :: Equ ix ix
data App f x = App (f x)
-- does not typecheck in 6.12.1 (but works in 6.10.4)
bar :: TF () () -> ()
bar (App Refl) = ()
-- does typecheck in 6.12.1 and 6.10.4
ar :: App (Equ ()) () -> ()
ar (App Refl) = ()
------------------
data family DF a :: Type -> Type
data instance DF () a = D (App (Equ ()) a)
bar_df :: DF () () -> ()
bar_df (D (App Refl)) = ()
|
