Skip to content

Instantly share code, notes, and snippets.

@Icelandjack Icelandjack/14733.hs
Created Jan 31, 2018

Embed
What would you like to do?
14733.hs
{-# Language QuantifiedConstraints #-}
{-# Language GADTs #-}
{-# Language ConstraintKinds #-}
{-# Language MultiParamTypeClasses #-}
{-# Language UndecidableSuperClasses #-}
{-# Language FlexibleInstances #-}
{-# Language UndecidableInstances #-}
{-# Language AllowAmbiguousTypes #-}
data D c where
D :: c => D c
class f a => AppC f a
instance f a => AppC f a
proof :: (forall xx. AppC f xx) => D (f a)
proof = D
----
{-
Curiously this requires '-XAllowAmbiguousTypes'!
• Could not deduce: f xx
from the context: forall xx. AppC f xx
bound by the type signature for:
proof :: forall (f :: * -> Constraint) a.
(forall xx. AppC f xx) =>
D (f a)
at /tmp/AAA.hs:15:10-42
• In the ambiguity check for ‘proof’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: proof :: (forall xx. AppC f xx) => D (f a)
|
15 | proof :: (forall xx. AppC f xx) => D (f a)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-}
{-
Final error message:
• Could not deduce: f a arising from a use of ‘D’
from the context: forall xx. AppC f xx
bound by the type signature for:
proof :: forall (f :: * -> Constraint) a.
(forall xx. AppC f xx) =>
D (f a)
at /tmp/AAA.hs:16:1-42
• In the expression: D
In an equation for ‘proof’: proof = D
• Relevant bindings include
proof :: D (f a) (bound at /tmp/AAA.hs:17:1)
|
17 | proof = D
| ^
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.