Add GHCi help message for :def! and :: commands
[ghc.git] / testsuite / tests / typecheck / should_compile / T15141.hs
1 {-# LANGUAGE PolyKinds, TypeFamilies, TypeFamilyDependencies,
2 ScopedTypeVariables, TypeOperators, GADTs,
3 DataKinds #-}
4
5 module T15141 where
6
7 import Data.Type.Equality
8 import Data.Proxy
9
10 type family F a = r | r -> a where
11 F () = Bool
12
13 data Wumpus where
14 Unify :: k1 ~ F k2 => k1 -> k2 -> Wumpus
15
16 f :: forall k (a :: k). k :~: Bool -> ()
17 f Refl = let x :: Proxy ('Unify a b)
18 x = undefined
19 in ()
20
21 {-
22 We want this situation:
23
24 forall[1] k[1].
25 [G] k ~ Bool
26 forall [2] ... . [W] k ~ F kappa[2]
27
28 where the inner wanted can be solved only by taking the outer
29 given into account. This means that the wanted needs to be floated out.
30 More germane to this bug, we need *not* to generalize over kappa.
31
32 The code above builds this scenario fairly exactly, and indeed fails
33 without the logic in kindGeneralize that excludes constrained variables
34 from generalization.
35 -}