- Section CV.
-
- (* the PHOAS type which stands for coercion variables of System FC *)
-
-
- (* Figure 7: γ, δ *)
- Inductive RawHaskCoer {CV:Type} : RawCoercionKind -> Prop := (* FIXME *).
-(*
- | CoVar : CV -> RawHaskCoer (* g *)
- | CoType : RawHaskType -> RawHaskCoer (* τ *)
- | CoApp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* γ γ *)
- | CoAppT : RawHaskCoer -> RawHaskType -> RawHaskCoer (* γ@v *)
- | CoCFApp : ∀ n, CoFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* C γⁿ *)
- | CoTFApp : ∀ n, TyFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* S_n γⁿ *)
- | CoAll : Kind -> (TV -> RawHaskCoer) -> RawHaskCoer (* ∀a:κ.γ *)
- | CoSym : RawHaskCoer -> RawHaskCoer (* sym *)
- | CoComp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* ◯ *)
- | CoLeft : RawHaskCoer -> RawHaskCoer (* left *)
- | CoRight : RawHaskCoer -> RawHaskCoer (* right *).
-*)
- End CV.
+ (* Figure 7: γ, δ; CV is the PHOAS type which stands for coercion variables of System FC *)
+ Inductive RawHaskCoer {CV:Type} : RawCoercionKind -> Prop := .
+ (*
+ * This has been disabled until we manage to reconcile SystemFC's
+ * coercions with what GHC actually implements (they are not the
+ * same!)
+ *
+ | CoVar : CV -> RawHaskCoer (* g *)
+ | CoType : RawHaskType -> RawHaskCoer (* τ *)
+ | CoApp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* γ γ *)
+ | CoAppT : RawHaskCoer -> RawHaskType -> RawHaskCoer (* γ@v *)
+ | CoCFApp : ∀ n, CoFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* C γⁿ *)
+ | CoTFApp : ∀ n, TyFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* S_n γⁿ *)
+ | CoAll : Kind -> (TV -> RawHaskCoer) -> RawHaskCoer (* ∀a:κ.γ *)
+ | CoSym : RawHaskCoer -> RawHaskCoer (* sym *)
+ | CoComp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* ◯ *)
+ | CoLeft : RawHaskCoer -> RawHaskCoer (* left *)
+ | CoRight : RawHaskCoer -> RawHaskCoer (* right *).
+ *)