summaryrefslogtreecommitdiff
path: root/testsuite/tests/dependent/should_compile/T14845_compile.hs
blob: c059f1d5e9071a0e38b440bce2471228208ddcd4 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
{-# Language PolyKinds, DataKinds, KindSignatures, GADTs, ConstraintKinds #-}
{-# Language FlexibleContexts #-}
{-# Language RankNTypes #-}
{-# Language TypeOperators #-}
module T14845 where

import Data.Kind
import Data.Type.Equality

data A :: Type -> Type where
  MkA1 :: a ~  Int => A a
  MkA2 :: a ~~ Int => A a

data SA :: forall a. A a -> Type where
  SMkA1 :: SA MkA1
  SMkA2 :: SA MkA2