Commit 81c20b80 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Cant unify under an implication

parent 1897f97c
......@@ -15,7 +15,7 @@ ntI = undefined
foo :: forall m n. EQ_ (Maybe m) (Maybe n)
foo = ntI (`eqE` (eqI :: EQ_ m n))
-- This works:
-- Alternative
-- foo = ntI (\eq -> eq `eqE` (eqI :: EQ_ m n))
-- eq :: EQ_ (Maybe m) (Maybe n)
Couldn't match type `z' with `n'
`n' is a rigid type variable bound by
the type signature for `foo' at Simple14.hs:16:17
because z is untouchable
inside the constraints (Maybe m ~ Maybe n)
bound at the polymorphic type `x ~ y => EQ_ z z'
In the second argument of `eqE', namely `(eqI :: EQ_ m n)'
In the first argument of `ntI', namely `(`eqE` (eqI :: EQ_ m n))'
In the expression: ntI (`eqE` (eqI :: EQ_ m n))
......@@ -14,7 +14,7 @@ test('Simple10', normal, compile, [''])
test('Simple11', normal, compile, [''])
test('Simple12', normal, compile, [''])
test('Simple13', expect_fail, compile, [''])
test('Simple14', normal, compile, [''])
test('Simple14', normal, compile_fail, [''])
test('Simple15', normal, compile, [''])
test('Simple16', normal, compile, [''])
test('Simple17', normal, compile, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment