Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Contractiveness check unsound with constraints #7374

Closed
vicuna opened this issue Sep 26, 2016 · 3 comments
Closed

Contractiveness check unsound with constraints #7374

vicuna opened this issue Sep 26, 2016 · 3 comments
Assignees
Labels
bug typing typing-GADTS GADT typing and exhaustiveness bugs
Milestone

Comments

@vicuna
Copy link

vicuna commented Sep 26, 2016

Original bug ID: 7374
Reporter: @lpw25
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2016-09-29T08:42:39Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.04.0 +dev / +beta1 / +beta2
Target version: 4.04.0 +dev / +beta1 / +beta2
Fixed in version: 4.04.0 +dev / +beta1 / +beta2
Category: typing
Child of: #5998
Monitored by: @gasche @yallop

Bug description

The contractiveness check ignores constraints, which makes it unsound. For example:

type ('a, 'b) eq = Refl : ('a, 'a) eq

let trans : type a b x . (a, x) eq -> (b, x) eq -> (a, b) eq =
fun Refl Refl -> Refl

let cast : type a b . (a, b) eq -> a -> b =
fun Refl x -> x

module type S = sig
type 'a t constraint 'a = [`Rec of 'b]
end

module Fix (X : S) : sig
type t
val uniq : ('a, [Rec of 'a] X.t) eq -> ('a, t) eq end = struct type t = [Rec of 'a] X.t as 'a
let uniq : type a . (a, [`Rec of a] X.t) eq -> (a, t) eq =
fun Refl -> Refl
end

module Id = struct
type 'a t = 'b
constraint 'a = [ `Rec of 'b ]
end

module Bad = Fix(Id)

let segfault () =
print_endline
(cast (trans (Bad.uniq Refl) (Bad.uniq Refl)) 0)

;; segfault ()

I think the fix is to consider:

[`Rec of 'a] X.t

as non-contractive when X.t has a constraint of the form [`Rec of 'a].

@vicuna
Copy link
Author

vicuna commented Sep 29, 2016

Comment author: @garrigue

Fixed in 4.04 by commit aec371d.

Actually the problem was not in the contractiveness check itself, but in the handling of arguments of non-contractive types: since they are not contractive, we must assume that subcomponents could be extracted, and any occurence could be returned.

@vicuna vicuna closed this as completed Sep 29, 2016
@vicuna
Copy link
Author

vicuna commented Sep 29, 2016

Comment author: @lpw25

I'm not sure, but isn't that overly conservative? In general subcomponents cannot be extracted. They can only be extracted when they appear in the constraints on the type's parameters.

@vicuna
Copy link
Author

vicuna commented Sep 30, 2016

Comment author: @garrigue

It is true, but better safe than sorry, and this check is only about trying to create a recursive type involving an abstract type using a GADT unification , not very usual code.
In particular, if we allow this for non-constrained type parameters, we need a way to check that we really have the type definition at hand: recall that when the compiler does not find a .cmi, it can still handle a type as abstract, without a proper definition, and in particular without information about the constraints.

@vicuna vicuna added the typing label Mar 14, 2019
@vicuna vicuna added this to the 4.04.0 milestone Mar 14, 2019
@vicuna vicuna added the bug label Mar 20, 2019
@Octachron Octachron added the typing-GADTS GADT typing and exhaustiveness bugs label May 18, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug typing typing-GADTS GADT typing and exhaustiveness bugs
Projects
None yet
Development

No branches or pull requests

3 participants