Use method type signatures if given

Fixes #54.

src/Frontend/Declassify.hs

@@ -164,12 +164,12 @@ deinstance qname@(QName modName name) loc (PatInstanceDef methods) typ = located
               $ Clause mempty
               $ abstractNone
               $ apps (Con $ HashSet.singleton $ classConstr className)
-              $ (\(n, _, _) -> (Explicit, global $ mname n)) <$> methods'
+              $ (\(n, _, _, _) -> (Explicit, global $ mname n)) <$> methods'
           , Just typ
           )
           :
-          [ (mname n, loc', TopLevelPatDefinition def, Nothing)
-          | (n, loc', def) <- Vector.toList methods'
+          [ (mname n, loc', TopLevelPatDefinition def, mtyp)
+          | (n, loc', def, mtyp) <- Vector.toList methods'
           ]
   where
     diff xs ys = HashSet.toList $ HashSet.difference (toHashSet xs) (toHashSet ys)
@@ -178,7 +178,7 @@ deinstance qname@(QName modName name) loc (PatInstanceDef methods) typ = located
         p [] = False
         p [_] = False
         p _ = True
-    getName = fst3
+    getName (n, _, _, _) = n
 
 getClass
   :: Expr v

src/Frontend/ScopeCheck.hs

@@ -149,7 +149,7 @@ scopeCheckTopLevelDefinition (Unscoped.TopLevelInstanceDefinition typ ms) = do
   let res = Scoped.TopLevelPatInstanceDefinition
         $ Scoped.PatInstanceDef
         $ Vector.fromList
-        $ (\(loc, (n, (d, _typ))) -> (n, loc, d)) -- TODO use the type
+        $ (\(loc, (n, (d, mtyp))) -> (n, loc, d, mtyp))
         <$> ms'
   return (res, Just typ')
 

src/Syntax/Concrete/Definition.hs

@@ -29,7 +29,7 @@ data PatDefinition clause
   = PatDefinition Abstract IsInstance (NonEmpty clause)
   deriving (Foldable, Functor, Show, Traversable)
 
-newtype PatInstanceDef expr v = PatInstanceDef (Vector (Name, SourceLoc, PatDefinition (Clause Void expr v)))
+data PatInstanceDef expr v = PatInstanceDef (Vector (Name, SourceLoc, PatDefinition (Clause Void expr v), Maybe (expr v)))
   deriving (Foldable, Functor, Show, Traversable)
 
 data Clause b expr v = Clause
@@ -70,7 +70,7 @@ instance GlobalBound TopLevelPatDefinition where
   bound f g (TopLevelPatInstanceDefinition instanceDef) = TopLevelPatInstanceDefinition $ bound f g instanceDef
 
 instance GlobalBound PatInstanceDef where
-  bound f g (PatInstanceDef ms) = PatInstanceDef $ second (bound f g <$>) <$> ms
+  bound f g (PatInstanceDef ms) = PatInstanceDef $ (\(name, loc, def, mtyp) -> (name, loc, bound f g <$> def, bind f g <$> mtyp)) <$> ms
 
 instance GlobalBound (Clause b) where
   bound f g (Clause pats s) = Clause (fmap (first (bound f g)) <$> pats) (bound f g s)
@@ -107,9 +107,10 @@ instance PrettyNamed clause => PrettyNamed (PatDefinition clause) where
 deriveEq1 ''PatDefinition
 
 instance (Pretty (expr v), Monad expr, IsString v) => PrettyNamed (PatInstanceDef expr v) where
-  prettyNamed name (PatInstanceDef ms)
-    = name <+> "=" <+> "instance" <+> "where" <$$>
-    indent 2 (vcat $ (\(n, _, m) -> prettyNamed (prettyM n) m) <$> ms)
+  prettyNamed name (PatInstanceDef ms) = name <+> "=" <+> "instance" <+> "where" <$$> do
+    let go (n, _, m, Nothing) = prettyNamed (prettyM n) m
+        go (n, _, m, Just typ) = prettyM n <+> ":" <+> prettyM typ <$$> prettyNamed (prettyM n) m
+    indent 2 (vcat $ go <$> ms)
 
 instantiateClause
   :: Monad expr

tests/success/classes/MethodSignature.vix

@@ -0,0 +1,14 @@
+type Maybe a
+  = Nothing
+  | Just a
+
+type Maybe2 a
+  = Nothing
+  | Just a
+
+class Pointed f where
+  point : forall a. a -> f a
+
+instance Pointed Maybe where
+  point : forall a. a -> Maybe a
+  point = Just

tests/type-error/classes/MethodSignature.vix

@@ -0,0 +1,10 @@
+type Maybe a
+  = Nothing
+  | Just a
+
+class Pointed f where
+  point : forall a. a -> f a
+
+instance Pointed Maybe where
+  point : Int
+  point = Just