hpc 2017-02-09 12:53:18
Jello_Raptor: maybe it has to do with type families being closer to aliases than to data definitions
hpc 2017-02-09 12:53:29
so when you write an instance for one, it's not really a well-defined type
hpc 2017-02-09 12:54:19
unwanted constructors are pretty much inevitable when you want to do stuff with type classes though
hpc 2017-02-09 12:54:25
what with the newtyping you often have to do
nshepperd 2017-02-09 12:55:28
type families aren't type constructors
nshepperd 2017-02-09 12:56:52
so you can't make a type class instance on them
ion 2017-02-09 12:58:38
Hi, would it be possible for this type to be inferred? https://gist.github.com/ion1/ae343d4c6369cfe048913c6b6b88e12f
nshepperd 2017-02-09 12:58:44
although, now you can make type checker plugins that will produce such instances on demand, then it's up to you to make sure your instances are correct and coherent...
ion 2017-02-09 12:59:18
I know dependent types are incompatible with type inference in general, but it seems to me this specific case should have no ambiguity.
ion 2017-02-09 13:00:16
Not that DataKinds are even necessary for this, actually
benzrf 2017-02-09 13:02:05
ion: thats not dependent types
benzrf 2017-02-09 13:02:11
jsyk
nshepperd 2017-02-09 13:03:25
ion: I think the Vect _ a -> a part could be inferred in theory
nshepperd 2017-02-09 13:04:28
ion: but ghc just gives up on inference for GADTs in general, because of this: is that a total function Vect (S Z) a -> a, or a partial function Vect n a -> a?
dmwit 2017-02-09 13:04:38
ion: If we write `type family Foo n a; type instance Foo (S Z) a = a`, then this also has type `Vect n a -> Foo n a`, which doesn't unify with the type you gave.
nshepperd 2017-02-09 13:05:09
also that
dmwit 2017-02-09 13:05:27
ion: (And there is no type that generalizes both your type and this one.)
ion 2017-02-09 13:05:37
Thanks for your comments.
dmwit 2017-02-09 13:07:04
So I think the answer to your question is that yes, that type could be inferred in principle. But so could other types, and then who's to say which is the best one? Presumably the answer here is "the user should say which is best". And that's the answer GHC chose.
ion 2017-02-09 13:09:22
Is there a way to do "do a :- b :- c :- Nil <- generateStuff", passing the number of outputs to generateStuff implicitly instead of explicitly? "do a :- b ;- c :- Nil <- generateStuff (SS (SS (SS SZ)))" (with singleton types) works and typechecks but I'm having trouble finding a way to infer it.
MarcelineVQ 2017-02-09 13:22:22
@tell merijn made a couple suggestions as paste annotations, hopefully they're relevant, hard to say for sure without the types and imports :> http://lpaste.net/6298367134955208704
lambdabot 2017-02-09 13:22:22
Consider it noted.
