Encode shape information in `PmOracle`
[ghc.git] / testsuite / tests / pmcheck / complete_sigs / T13717.hs
1 {-# OPTIONS_GHC -Wincomplete-patterns #-}
2 {-# LANGUAGE DataKinds #-}
3 {-# LANGUAGE PatternSynonyms #-}
4 {-# LANGUAGE ScopedTypeVariables #-}
5 {-# LANGUAGE GADTs #-}
6 {-# LANGUAGE KindSignatures #-}
7 {-# LANGUAGE ViewPatterns #-}
8 {-# LANGUAGE Trustworthy #-}
9 {-# LANGUAGE EmptyCase #-}
10
11 module Fin (Nat (..), Fin (FZ, FS)) where
12 import Numeric.Natural
13 import Unsafe.Coerce
14
15 data Nat = Z | S Nat
16
17 -- Fin *must* be exported abstractly (or placed in an Unsafe
18 -- module) to maintain type safety.
19 newtype Fin (n :: Nat) = Fin Natural
20
21 data FinView n where
22 VZ :: FinView ('S n)
23 VS :: !(Fin n) -> FinView ('S n)
24
25 viewFin :: Fin n -> FinView n
26 viewFin (Fin 0) = unsafeCoerce VZ
27 viewFin (Fin n) = unsafeCoerce (VS (Fin (n - 1)))
28
29 pattern FZ :: () => n ~ 'S m => Fin n
30 pattern FZ <- (viewFin -> VZ) where
31 FZ = Fin 0
32
33 pattern FS :: () => n ~ 'S m => Fin m -> Fin n
34 pattern FS m <- (viewFin -> VS m) where
35 FS (Fin m) = Fin (1 + m)
36
37 {-# COMPLETE FZ, FS #-}
38
39 finZAbsurd :: Fin 'Z -> a
40 finZAbsurd x = case x of
41