I just realized that the "implicit pattern match" is nonsense, as it's not indicated at compile time which constructor the pattern match resulted in.
So something more like:
ev :: SomeSing Nat > Some1 EmptyVec
ev s =
case forall n. SingI n => sing @n of
SNat >  Constraint brought into scope: (forall n. SingI n => KnownNat n)
readKnowingTypeIndex s "EmptyVec"
Also makes it clear that the expression is being evaluated.
I end up wishing that I could put myself in some sort of context where I claim that "n
could be anything, and suppose we have SingI n
", so that I'm allowed to call singIToKnownNat @n
. In this context, the fact that we're able to produce a Dict (KnownNat n)
, should prove to the compiler that forall n. SingI n => KnownNat n
.
The expression that you provide in this context would get implicitly pattern matched, in order to learn the constraints that can result from the assumption made in the context. The compiler concludes that the assumed constraint implies the constraints found by the implicit pattern match.
I'll make up some syntax for this. Imagine a suppose ... in ...
keyword:
ev :: SomeSing Nat > Some1 EmptyVec
ev s =
suppose forall (n :: Nat). SingI n =>
singIToKnownNat @n
in
readKnowingTypeIndex s "EmptyVec"
It's a funny mix of type level and expression level syntax. singIToKnownNat @n
soundly returns a Dict (KnownNat n)
, and pattern matching on the resulting Dict
constructor would make us learn that for all n
, SingI n
(from the suppose
context) implies KnownNat n
.
In fact this has nothing to do with Dict
. The following would work equally well:
ev :: SomeSing Nat > Some1 EmptyVec
ev s =
suppose forall (n :: Nat). SingI n =>
sing @n
in
readKnowingTypeIndex s "EmptyVec"
since, after all, sing @n
returns an SNat :: Sing n
, which when pattern matched brings KnownNat n
into scope.
I don't mean to pollute language syntax. If there's a way to avoid new syntax, like a magical builtin function, that's preferable. It also has to be able to quantify over various numbers of type variables, so I don't think the builtin function that I proposed in the description would even work in this practical case.
I'm a bit curious. When I try to write
suppose1 :: forall a b r. (forall x. a x => Dict (b x)) > ((forall x. a x => b x) => r) > r
suppose1 Dict a = a
GHC complains already on the type signature: Could not deduce: b x
. What's going on there?
I wouldn't be surprised if it's already possible today to write something magical using unsafeCoerce that works for specific cases, in the style of Edward Kmett's reflection
package. But that's not a longterm solution.
Here's a motivating example where I wish that I was able to show the compiler that one (quantified) constraint implies another. In this example, I'm using the singletons
library. The Data.Singletons.TypeLits
module contains
data instance Sing (n :: Nat) = KnownNat n => SNat
instance KnownNat n => SingI n where
sing = SNat
where the compiler learns of the implication forall n. KnownNat n => SingI n
. However the reverse implication forall n. SingI n => KnownNat n
is also true as evidenced by:
data Dict :: Constraint > Type where
Dict :: c => Dict c
singIToKnownNat :: forall n. SingI n => Dict (KnownNat n)
singIToKnownNat = case sing @n of SNat > Dict
The crux is that there's is no way to rephrase singIToKnownNat
in terms of constraint implication:
singIImpliesKnownNat :: forall r. ((forall n. SingI n => KnownNat n) => r) > r
singIImpliesKnownNat a = undefined  Can't implement this?
What this ticket asks for is some way to write a correct definition of things like singIImpliesKnownNat
. Something similar to the definition of singIToKnownNat
, I would imagine.
Here's the full example code:
 GHC 8.6.2, Singletons 2.5
{# LANGUAGE GADTs #}
{# LANGUAGE TypeInType #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE QuantifiedConstraints #}
module ReifyImplications where
import Data.Kind
import GHC.TypeNats
import Data.Singletons
import Data.Singletons.TypeLits
import Data.Type.Equality
data EmptyVec :: Nat > Type where
EmptyVec :: EmptyVec 0
instance KnownNat n => Read (EmptyVec n) where
readsPrec _ "EmptyVec" =
case sameNat @n @0 Proxy Proxy of
Just Refl > [(EmptyVec, "")]
Nothing > []
data Some1 :: (k > Type) > Type where
Some1 :: Sing a > f a > Some1 f
readKnowingTypeIndex ::
forall k (f :: k > Type). (forall x. SingI x => Read (f x)) =>
SomeSing k > String > Some1 f
readKnowingTypeIndex (SomeSing s) str =
Some1 s $ withSingI s $ read str
readKnowingNat ::
forall (f :: Nat > Type). (forall n. KnownNat n => Read (f n)) =>
SomeSing Nat > String > Some1 f
readKnowingNat (SomeSing (SNat :: Sing a)) str =
Some1 (SNat @a) $ read str  Can't write this in terms of readKnowingTypeIndex?
ev :: SomeSing Nat > Some1 EmptyVec
ev s = readKnowingTypeIndex s "EmptyVec"  Could not deduce (KnownNat x).
ev s = readKnowingNat s "EmptyVec"  OK, but this doesn't work on every kind. Only Nat.
singIImpliesKnownNat :: forall r. ((forall n. SingI n => KnownNat n) => r) > r
singIImpliesKnownNat a = undefined  Can't implement this?
ev s =
singIImpliesKnownNat $
readKnowingTypeIndex s "EmptyVec"  OK, if singIImpliesKnownNat was real.
 Now, this is easy to implement. But it's not practically usable in the definition of `ev`.
data Dict :: Constraint > Type where
Dict :: c => Dict c
singIToKnownNat :: forall n. SingI n => Dict (KnownNat n)
singIToKnownNat = case sing @n of SNat > Dict
 Bonus: readKnowingNat written in terms of readKnowingTypeIndex
readKnowingNat' ::
forall (f :: Nat > Type). (forall n. KnownNat n => Read (f n)) =>
SomeSing Nat > String > Some1 f
readKnowingNat' s str =
singIImpliesKnownNat $
readKnowingTypeIndex s str
#15635 (closed) Describes the same problem, perhaps in a clearer way.
Trac field  Value 

Related  #14822 (closed) → #14822 (closed), #15635 (closed) 
Trac field  Value 

Related   → #14937 
CC   → Bj0rn 
This is the same as #14937.
Consider this code which successfully compiles:
{# LANGUAGE TypeInType, TypeFamilies, GADTs #}
module Bug where
class HasIndex a where
type Index a
emptyIndex :: IndexWrapper a
instance HasIndex [a] where
type Index [a] = Int
emptyIndex = Wrap 0
data IndexWrapper a where
Wrap :: Index a > IndexWrapper a
type family UnwrapAnyWrapperLikeThing (a :: t) :: k
type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a
The mere act of moving the definition of IndexWrapper
anywhere below the definition of UnwrapAnyWrapperLikeThing
makes the type family instance at the bottom of the example fail compilation, with this error:
Bug.hs:17:15: error:
• Illegal type synonym family application in instance: Index [b]
• In the type instance declaration for ‘UnwrapAnyWrapperLikeThing’

17  type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
This is the smallest example that I could come up with; my real scenario of course has more things going on, but I can share if it would help.
The problem for me (other than that I'm pretty sure reordering definitions in Haskell should never affect anything) is that I would like just the definition of the type family (UnwrapAnyWrapperLikeThing
in this example) in module A
and all of the other definitions in module B
that imports A
.
Ideally, I would have liked to add a HasIndex a
constraint to the Wrap
constructor, but that disqualifies use of 'Wrap
on the type level. This does make me feel like I'm on shaky ground to begin with.
I have reproduced this bug on 8.2.2, 8.4.3 and 8.6.0.20180810 (NixOS). I should note that 8.0.2 rejects even the code that I pasted here.
Trac field  Value 

Version  8.4.3 
Type  Bug 
TypeOfFailure  OtherFailure 
Priority  normal 
Resolution  Unresolved 
Component  Compiler 
Test case  
Differential revisions  
BlockedBy  
Related  
Blocking  
CC  
Operating system  
Architecture 
This is possibly the same question as #14822, asked in more general terms. Would it be viable/sound to have a way of extracting implication constraints out of terms which effectively encode such constraints, such as (:)
from Data.Constraint
?
Here's how I think about it. a : b
is equivalent to forall r. a => (b => r) > r
. This is a type that, as I read it, expresses "if you can show a
, then I can show b
". This is very similar to forall r. ((a => b) => r) > r
, which expresses "(without obligations) I can show that a
implies b
".
It seems to me (and I know this is handwavy) like expressions of both of these types actually must have the same "knowledge", i.e. that a
imples b
. Is this actually correct?
I am wondering whether we could have a builtin function like:
reifyImplication :: forall a b. (forall r. a => (b => r) > r) > (forall r. ((a => b) => r) > r)
We can already write the function that goes the other direction.
There are plenty of ways to represent this conversion. Some more straightforward, using a : b
or Dict a > Dict b
. I just went with one that doesn't require any types beyond arrows.
I'm curious about the soundness of this. I have tried really hard to implement this function, but I don't think it can be done.
I don't know if this proves anything, but replacing (=>)
with (>)
and all constraints c
with Dict c
, this function can be written:
dictReifyImplication :: forall a b. (forall r. Dict a > (Dict b > r) > r) > (forall r. ((Dict a > Dict b) > r) > r)
dictReifyImplication f g = g (\a > f a id)
Trac field  Value 

Version  8.5 
Type  FeatureRequest 
TypeOfFailure  OtherFailure 
Priority  normal 
Resolution  Unresolved 
Component  Compiler 
Test case  
Differential revisions  
BlockedBy  
Related  #14822 
Blocking  
CC  
Operating system  
Architecture 