From eca3f65315aae5923bd3d6dc6c3dcfe20da8866b Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 25 Jul 2017 12:28:29 +0200 Subject: Extraction: do not mix Haskell types Any and () (revert 8e257d4, fix bugs 4844 and 4824) The commit 8e257d4 (which consider the dummy type Tdummy to be polymorphic and hence immune of the need for unsafeCoerce) is quite wrong, even if in pratice it worked ok most of the time. The confusion comes from the fact that the dummy value (__ aka MLdummy internally) is implemented in Haskell as Prelude.error, hence it has indeed a polymorphic unrestricted type. But the dummy type Tdummy used when extracting types must be monomorphic (otherwise type parameters would have to be propagated out of any type definition involving Tdummy). We implement Tdummy by Haskell's (), which for instance isn't convertible to Any, as shown by the examples in bug reports 4844 and 4824. This fix will bring back some more unsafeCoerce in Haskell extraction, including possibly a few spurious ones. And these extra unsafeCoerce might also hinder further code optimisations. We tried to mitigate that by directly removing [MLmagic] constructors in front of [MLdummy _]. NB: even if the original bug report mentions universe polymorphism, this issue is almost unrelated to it. It just happens that when universe polymorphism is off, an inductive instance is fully placed in Prop (cf. template polymorphism) in the example, avoiding triggering the issue. Warning: the test-suite file is there for archiving the repro case, but currently it doesn't test much (we should run ghc on the extracted code). --- plugins/extraction/mlutil.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index f1bcde2f3..a4c2bcd88 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -120,7 +120,6 @@ let rec mgu = function mgu (a, a'); mgu (b, b') | Tglob (r,l), Tglob (r',l') when Globnames.eq_gr r r' -> List.iter mgu (List.combine l l') - | (Tdummy _, _ | _, Tdummy _) when lang() == Haskell -> () | Tdummy _, Tdummy _ -> () | Tvar i, Tvar j when Int.equal i j -> () | Tvar' i, Tvar' j when Int.equal i j -> () @@ -1052,6 +1051,7 @@ let rec simpl o = function | MLmagic(MLcase(typ,e,br)) -> let br' = Array.map (fun (ids,p,c) -> (ids,p,MLmagic c)) br in simpl o (MLcase(typ,e,br')) + | MLmagic(MLdummy _ as e) when lang () == Haskell -> e | MLmagic(MLexn _ as e) -> e | a -> ast_map (simpl o) a -- cgit v1.2.3